c_reports_exact
plain-language theorem explainer
The theorem establishes that the RS-native speed of light, converted through a single-anchor calibration certificate, equals exactly 299792458 m/s. Researchers reporting RS-native computations in SI units would cite it to confirm definitional consistency with the 2019 meter redefinition. The proof is a one-line wrapper that applies the c_in_si theorem to the certificate-derived calibration and simplifies against the external c_SI anchor.
Claim. Let cert be a calibration certificate supplying the single empirical scalar τ₀ (seconds per tick) together with protocol and positivity conditions. Then the SI-unit conversion of the RS-native speed of light (equal to 1 voxel per tick) yields exactly c_SI = 299792458 m/s.
background
The module supplies a single-anchor SI calibration protocol for RS-native measurements. RS-native theory runs in tick/voxel/coh/act units with c = 1 and no SI numerals; a single measured scalar τ₀ in seconds is supplied, after which meters_per_voxel is fixed by the SI definition of c and joules_per_coh follows from the SI definition of h (hence ħ) together with the identity 1 act = 1 coh × 1 tick. CalibrationCert is the structure that bundles τ₀, the canonical protocol predicate, and the derived ExternalCalibration used for reporting. The upstream theorem c_in_si states that to_m_per_s cal c = 299792458 for any ExternalCalibration cal whose speed_consistent field holds.
proof idea
The proof is a one-line wrapper. It invokes the upstream theorem c_in_si on the ExternalCalibration obtained from the certificate, then applies simpa with the definition of c_SI to discharge the goal.
why it matters
This theorem closes the single-anchor calibration loop in the Measurement.RSNative.Calibration.SingleAnchor module, guaranteeing that the RS-native c = 1 reports the exact SI value without fit parameters. It supports the overall framework by providing a hygienic interface between native computations and experimental SI anchors, consistent with the exact 2019 redefinition of the meter and the module's design that everything beyond τ₀ is derived or definitional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.