c_SI
The declaration supplies the exact SI speed of light 299792458 m/s as the fixed calibration seam between RS-native units and laboratory measurements. Cosmologists comparing RS-derived ratios such as Hubble constants or Planck scales to SH0ES or CODATA data invoke this constant to express results in km/s/Mpc or meters. It is introduced by direct numerical assignment of the 2019 SI redefinition value with no further computation.
claimThe speed of light in vacuum is defined by the exact numerical value $c = 299792458$ m/s fixed by the 2019 SI redefinition.
background
The module establishes the SI calibration seam required once RS derives all physics in native units where $c = 1$. The Planck scale supplies the bridge: in RS-native units the Planck length equals $1/√π$, while its SI value remains an external experimental input. The module therefore supplies only the conversion constants and ratios, not the SI numbers themselves. Upstream definitions in ExternalAnchors and SingleAnchor supply the identical numerical anchor with the explicit label EXTERNAL ANCHOR for the 2019 SI value.
proof idea
Direct definition that assigns the integer 299792458 to the real number c_SI.
why it matters in Recognition Science
This constant anchors every downstream conversion in the cosmology module, including the positivity lemma c_SI_pos and the structure SICalibrationCert that certifies consistency between Planck length, Planck time, and c_SI. It implements the reporting seam described in the module documentation, allowing RS-native predictions (c = 1) to be compared with observed quantities while keeping the SI values external. The declaration closes the calibration path used by 14 downstream sites, including calibration_protocol_hygienic and si_calibration_cert.
scope and limits
- Does not derive the numerical value from any RS equation or forcing chain.
- Does not claim the value is predicted or measured inside Recognition Science.
- Does not alter the native-unit statement c = 1.
- Does not provide error bounds or uncertainty; the value is treated as exact by definition.
Lean usage
theorem c_SI_pos : 0 < c_SI := by unfold c_SI; norm_numformal statement (Lean)
54def c_SI : ℝ := 299792458
proof body
Definition body.
55
56/-- 1 Megaparsec in meters (IAU 2012 definition).
57 1 pc = 648000/π AU, 1 AU = 149597870700 m (exact). -/