sigmaVal
plain-language theorem explainer
sigmaVal extracts the standard deviation from a symmetric uncertainty report in the RS-native measurement scaffold. Measurement protocols cite it when converting Uncertainty instances to numeric values for ledger observables. The definition is a direct pattern match on the Uncertainty inductive type that returns the embedded real for the sigma constructor and none otherwise.
Claim. Let $u$ be an uncertainty report of type Uncertainty. Then $sigmaVal(u)$ returns some value $σ$ if $u$ is the symmetric 1σ constructor with $σ ≥ 0$, and returns none otherwise.
background
The RS-Native Measurement Framework (Core) supplies a Lean-first scaffold for scalar measurements using ticks, voxels, and ledger observables with $τ₀ = 1$. SI/CODATA calibration is deferred to external modules; every measurement carries an explicit protocol. Uncertainty is the lightweight inductive reporting seam with three constructors: sigma for symmetric standard deviation, interval for bounds, and discrete for finite distributions. This definition depends on the Uncertainty inductive (defined in the same module) together with two unrelated sigma abbreviations from decision theory and arithmetic functions.
proof idea
The definition is realized by exhaustive pattern matching on the Uncertainty constructors. The sigma case returns some σ; the interval and discrete cases return none. No lemmas or tactics are invoked; it is a direct structural match.
why it matters
sigmaVal supplies the numeric extraction step inside the measurement reporting seam, enabling downstream ledger observables to consume symmetric uncertainty reports. It sits inside the RS-native core that keeps protocols explicit and falsifiable. No parent theorems or downstream uses are recorded in the current graph, leaving open how interval and discrete cases will be lifted to the same numeric interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.