measure_to_joule_seconds
plain-language theorem explainer
This definition converts an RS-native action measurement (in act quanta) to SI joule-seconds by applying an external calibration record. A physicist extracting numerical predictions from Recognition Science would call it after supplying the calibration constants to produce conventional units. The implementation is a direct wrapper that maps the central value through scalar multiplication and scales the uncertainty bound by the same positive factor.
Claim. Given an external calibration record with positive joules-per-coherence and seconds-per-tick factors, and a measurement whose value is an action quantum, the result is the measurement whose value equals the original value multiplied by the product of those two factors, with uncertainty scaled by the same positive constant.
background
The module supplies the explicit interface that lets RS-native theory remain free of CODATA numerals while still allowing output in SI units. ExternalCalibration is the structure carrying the three conversion constants: seconds per tick, meters per voxel, and joules per coherence quantum. Measurement is the record type holding a name, central value, and error bound. The sibling definition to_joule_seconds multiplies an action quantum by joules_per_coh times seconds_per_tick; scaleUncertainty multiplies either a sigma or an interval uncertainty by a positive constant while preserving the non-negativity proof.
proof idea
The definition is a one-line wrapper that applies Measurement.map to the to_joule_seconds conversion on the value and Measurement.mapUncertainty to scaleUncertainty on the error component, using the product of the two positive calibration fields as the scaling factor.
why it matters
This adapter completes the seam between the RS-native core (governed by the Calibration axiom that fixes the second derivative of the cost functional at the origin to 1) and any external reporting requirement. It ensures that all Recognition Science derivations stay independent of empirical constants until an explicit ExternalCalibration record is supplied. No downstream theorems yet depend on it, so it functions as a terminal reporting utility rather than an internal lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.