scaleUncertainty
plain-language theorem explainer
scaleUncertainty multiplies an Uncertainty datum by a nonnegative real scalar while preserving its constructor structure. SI conversion helpers in the calibration module call it to propagate uncertainties when mapping RS-native measurements of ticks, voxels, or actions into SI units. The definition proceeds by direct case analysis on the three constructors of Uncertainty, scaling the numeric payload in each branch.
Claim. For real scalar $c$ with $c$ nonnegative and uncertainty representation $u$, the scaled uncertainty is obtained by multiplying the standard deviation (sigma case), both interval endpoints (interval case), or the value components of each support pair (discrete case) by $c$.
background
The module supplies explicit adapters that report RS-native quantities in SI units through an ExternalCalibration record supplied from outside the theory. Uncertainty is the inductive type defined in Core with three constructors: sigma for a nonnegative standard deviation, interval for closed bounds, and discrete for a finite list of (value, weight) pairs. The Core map function is used in the downstream conversion routines to apply both the value map and the uncertainty scaling in one step.
proof idea
The definition matches on the Uncertainty inductive. The sigma branch multiplies the deviation and re-proves nonnegativity via mul_nonneg. The interval branch multiplies both endpoints and invokes mul_le_mul_of_nonneg_right on the ordering hypothesis. The discrete branch applies map to the support list, scaling only the first component of each pair.
why it matters
The definition is invoked by the four measure_to_* functions that perform the actual RS-native to SI unit conversions while carrying uncertainty forward. It keeps the core Recognition theory free of CODATA numerals, satisfying the module rule that SI conversion occurs only through an externally supplied calibration record. It therefore supports the measurement reporting layer without altering the upstream forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.