intervalBounds
plain-language theorem explainer
intervalBounds extracts lower and upper limits from an interval uncertainty report inside the RS-native measurement scaffold. Measurement protocols that carry explicit bounds on scalar observables would cite this extractor when converting reports to concrete pairs. The definition is a direct pattern match on the Uncertainty inductive type that returns the pair for the interval case and none otherwise.
Claim. Let $U$ be the inductive type of uncertainty reports with constructors sigma, interval, and discrete. Define intervalBounds : $U$ → Option($ℝ$ × $ℝ$) by intervalBounds(interval($lo$, $hi$, _)) = some($lo$, $hi$) and intervalBounds($u$) = none for the sigma and discrete cases.
background
The module supplies a Lean-first measurement scaffold for Recognition Science in which every observable carries an explicit protocol. Uncertainty is the lightweight reporting seam for scalar values; its interval constructor records that the true value lies inside a closed interval [lo, hi] while the other constructors handle symmetric standard deviation and a finite discrete support list. The module document states that core theory remains RS-native (ticks, voxels, coherence) and that SI calibration lives outside this file.
proof idea
The definition is written by cases on the Uncertainty inductive type. It matches the interval constructor directly to return the supplied bounds and falls through to none for sigma and discrete.
why it matters
The definition supplies the basic accessor needed to read interval bounds inside the RS measurement core. It supports the module requirement that protocols remain explicit and that arbitrary choices cannot be hidden. No downstream declarations are recorded, so the extractor currently serves as an internal seam for later catalog modules that will consume bounded observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.