c_SI_pos
plain-language theorem explainer
The lemma states that the exact SI 2019 definition of the speed of light is strictly positive. Cosmology conversion and single-anchor calibration modules cite it to guarantee positive scaling when mapping RS-native units onto measured seconds and meters. The proof is a direct norm_num reduction on the integer constant 299792458.
Claim. $0 < c_{SI}$ where $c_{SI} := 299792458$ (exact SI 2019 value in m/s).
background
The ExternalAnchors module is the single quarantined location for all CODATA and empirical calibration data. Its policy forbids import by the cost-first core, so that Recognition Science derivations remain independent of measured values while still permitting later comparison. The definition c_SI records the exact 2019 SI value 299792458 m/s; upstream siblings in Cosmology.SIConversion and Measurement.RSNative.Calibration.SingleAnchor supply identical constants together with their own positivity statements.
proof idea
The lemma is a one-line wrapper that applies norm_num to the definition of c_SI, unfolding the integer literal and confirming the inequality by arithmetic evaluation.
why it matters
This positivity fact is required by externalCalibration_of_tau0_seconds, which builds the ExternalCalibration record from a single positive tau0_s by setting meters_per_voxel := c_SI * tau0_s. It therefore closes the mechanical link between the RS-native forcing chain (where c = 1) and the external SI anchors used for numerical checks. The module isolates such facts precisely to keep the RCL core free of empirical data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.