Uncertainty

formal source

  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)
 112  | _ => none
 113
 114end Uncertainty
 115
 116/-- A measurement value with protocol + (optional) time window + (optional) uncertainty. -/
 117structure Measurement (α : Type) where
 118  value : α
 119  window : Option Window := none
 120  protocol : Protocol
 121  uncertainty : Option Uncertainty := none
 122  notes : List String := []
 123
 124namespace Measurement
 125