measure_to_seconds
plain-language theorem explainer
The definition converts a Measurement of discrete ticks into an equivalent Measurement in real seconds. Researchers reporting RS-native simulation outputs in SI units would invoke it after supplying an ExternalCalibration record. It is realized as a direct composition of Measurement.map with the to_seconds converter and an uncertainty rescaler.
Claim. Given an external calibration record $cal$ containing the factor $s$ (seconds per tick) and a measurement $m$ whose value is expressed in ticks, the result is the measurement whose value equals the original value multiplied by $s$ and whose uncertainty is the original uncertainty multiplied by $s$ (using the positivity witness for $s$).
background
RS-native quantities are expressed in ticks, the atomic discrete time unit introduced in TimeEmergence as an ordered ledger index with no background manifold. The ExternalCalibration structure supplies the conversion factors, principally seconds_per_tick, that map these native units to SI without embedding CODATA numerals inside the theory or measurement catalogs. The Measurement structure packages a named quantity together with its central value and error bar; the sibling to_seconds function multiplies a tick count by the calibration factor to obtain seconds.
proof idea
The definition is a one-line wrapper. It first applies Measurement.mapUncertainty to rescale the input error using scaleUncertainty on the seconds_per_tick factor (with the witness le_of_lt cal.seconds_pos), then applies Measurement.map with to_seconds to convert the central value.
why it matters
This definition completes the explicit SI reporting seam for time measurements inside the RS-native calibration adapter. It preserves the independence of the core theory and measurement catalogs from external constants, directly supporting the eight-tick octave structure by supplying the conversion from the discrete Tick ledger to seconds. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.