Uncertainty
plain-language theorem explainer
The Uncertainty inductive type supplies three lightweight formats for reporting scalar measurement error in RS-native units: a non-negative standard deviation, a closed interval, or an unnormalized list of value-weight pairs. Groups producing RS observables such as ILG rotation curves or Hubble-tension predictions cite it to attach explicit error information while keeping protocols visible. The declaration is a direct inductive definition with no auxiliary lemmas or reduction rules.
Claim. An uncertainty report on a real scalar is one of: a standard deviation $σ$ with $σ ≥ 0$; a closed interval $[lo, hi]$ with $lo ≤ hi$; or a finite list of pairs $(value, weight)$.
background
The RS-Native Measurement Framework expresses observables in ticks, voxels, coherence (coh) and action (act) units with base time $τ_0 = 1$. Protocols must declare windowing and coarse-graining choices explicitly; the Uncertainty type is the reporting seam that carries those declarations without invoking full probability theory. Upstream ledger factorization and J-cost structures supply the underlying scalar quantities that receive these annotations.
proof idea
Direct inductive definition. The three constructors sigma, interval and discrete are introduced with their respective field types and the single inequality constraint on each; no tactics or lemmas are applied.
why it matters
This supplies the error vocabulary consumed by scaleUncertainty (SI calibration), intervalBounds extraction, mapUncertainty lifting, and the uncertainty fields inside ILGPrediction and H0_ILG. It closes the measurement seam required by the RS protocol discipline, allowing falsifiable predictions in FlybyAnomaly and HubbleTension modules to carry explicit bounds while remaining inside the core RS-native setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.