c_reports_exact
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not introduce any fit parameters beyond the single τ₀ scalar.
- Does not address multi-anchor or overdetermined calibration protocols.
- Does not compute numerical values for derived constants such as ħ.
formal statement (Lean)
140theorem c_reports_exact (cert : CalibrationCert) :
141 IndisputableMonolith.Constants.RSNativeUnits.to_m_per_s (calibration cert)
142 IndisputableMonolith.Constants.RSNativeUnits.c = c_SI := by
proof body
Term-mode proof.
143 -- This follows from the `speed_consistent` field plus `c_in_si`.
144 -- Note: RSNativeUnits.c = 1 (voxel/tick).
145 have := IndisputableMonolith.Constants.RSNativeUnits.c_in_si (calibration cert)
146 simpa [c_SI] using this
147
148/-- Under the derived calibration, 1 act reports \(\hbar\) in SI \(J·s\). -/