stop

formal source

  78
  79@[simp] def instant (t : Nat) : Window := ⟨t, 0⟩
  80
  81@[simp] def stop (w : Window) : Nat := w.t0 + w.len
  82
  83end Window
  84
  85/-! ## Uncertainty and measurement record -/
  86
  87/-- Uncertainty semantics for scalar (real-valued) measurements.
  88
  89v1 used only `sigma`. v2 adds:
  90- interval bounds
  91- a finite discrete distribution scaffold
  92
  93This is intentionally lightweight: it is a *reporting seam* for measurement,
  94not a full probability theory. -/
  95inductive Uncertainty where
  96  /-- Symmetric 1σ uncertainty (standard deviation), in the same units as the value. -/
  97  | sigma (σ : ℝ) (hσ : 0 ≤ σ)
  98  /-- Interval uncertainty: the true value lies in `[lo, hi]`. -/
  99  | interval (lo hi : ℝ) (hlohi : lo ≤ hi)
 100  /-- Finite discrete distribution scaffold: list of `(value, weight)` pairs.
 101      We do not require proof obligations (nonneg/sum=1) in v2; protocols must state hygiene. -/
 102  | discrete (support : List (ℝ × ℝ))
 103
 104namespace Uncertainty
 105
 106@[simp] def sigmaVal : Uncertainty → Option ℝ
 107  | sigma σ _ => some σ
 108  | _ => none
 109
 110@[simp] def intervalBounds : Uncertainty → Option (ℝ × ℝ)
 111  | interval lo hi _ => some (lo, hi)