mapUncertainty
plain-language theorem explainer
mapUncertainty applies a supplied transformation to the optional uncertainty field of a Measurement record while copying value, window, protocol, and notes unchanged. SI calibration routines cite it to rescale error intervals when converting RS-native observables such as Coh or Voxel into joules or meters. The definition performs a direct record update that delegates the transformation to the uncertainty component.
Claim. Given a map $f : Uncertainty → Uncertainty$ and a measurement $m : Measurement α$, the result has the same value, window, protocol, and notes as $m$, but with its uncertainty field replaced by the image of the original uncertainty under $f$ when that field is present.
background
In the RS-Native Measurement Framework a Measurement α carries a value of type α, an optional Window, a Protocol, an optional Uncertainty, and a list of notes. Uncertainty is an inductive type with three constructors: sigma for symmetric standard deviation, interval for closed bounds, and discrete for a finite support list. The module keeps all core observables in RS-native units (ticks, voxels, coh, act) and treats SI conversion as an external calibration step performed outside the core definitions.
proof idea
The definition is a direct record construction. It copies the value, window, protocol, and notes fields from the input measurement and replaces the uncertainty field by applying the supplied uMap to the original optional uncertainty.
why it matters
The declaration supplies the uncertainty-preserving counterpart to the sibling map function on values. It is invoked inside measure_to_joules, measure_to_meters, measure_to_seconds, and measure_to_joule_seconds to keep error reporting consistent during unit conversion from RS-native observables. This maintains the explicit protocol and uncertainty hygiene required by the measurement scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.