c_SI
plain-language theorem explainer
c_SI supplies the exact SI numerical value of the speed of light for anchoring derived constants to laboratory units. Cosmologists and metrologists in the Recognition framework cite it when converting RS-native quantities such as planck_length_SI to SI meters. The definition is a direct noncomputable assignment of 299792458 with no further computation or derivation.
Claim. $c_{SI} := 299792458$ (exact SI value of the speed of light in vacuum, in m/s, imported as calibration anchor).
background
The module derives physical constants from φ via the chain φ → E_coh → τ₀ → c → ℏ → G → α⁻¹. Here c is introduced as the ratio of fundamental length ℓ₀ to fundamental time τ₀, with the SI numerical value supplied by external calibration rather than internal derivation. The module doc states: 'Constants are derived, not assumed. SI values come from calibration.'
proof idea
Direct definition that assigns the integer 299792458 to a real number. It functions as a one-line wrapper importing the external anchor from Constants.ExternalAnchors.c_SI.
why it matters
This definition supplies the calibration anchor required by downstream results such as si_calibration_cert and SICalibrationCert in Cosmology.SIConversion. It completes the empirical link in the module's derivation chain while preserving the derived status of subsequent constants (ℏ, G, α⁻¹). The value matches the 2019 SI redefinition and is used to certify consistency between RS-native and SI units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.