c_SI_pos
plain-language theorem explainer
The speed of light in SI units is strictly positive. Researchers calibrating Recognition Science predictions to observational data in meters and seconds cite this fact when constructing external calibration objects. The proof is a one-line wrapper that unfolds the constant definition and reduces the inequality by normalization.
Claim. $0 < c_{SI}$ where $c_{SI} = 299792458$ is the exact SI value of the speed of light in meters per second.
background
Recognition Science works in native units with $c = 1$. The SIConversion module supplies the calibration seam that maps native predictions to SI observables via external anchors. Here $c_{SI}$ is defined as the 2019 SI exact value 299792458 m/s, independent of RS theory. Upstream results supply identical definitions and positivity statements in ExternalAnchors, SingleAnchor, and RRF.Foundation, each reducing to the same numerical constant.
proof idea
The proof is a one-line wrapper. It unfolds the definition of $c_{SI}$ to the literal 299792458 and applies norm_num to discharge the strict inequality.
why it matters
This lemma supplies the positivity hypothesis required by externalCalibration_of_tau0_seconds in SingleAnchor, which builds the full ExternalCalibration object used for RS-to-SI conversion of cosmological observables. It closes a basic requirement in the SI calibration seam without deriving the numerical value from theory. The result supports the bridge between native units ($c=1$) and human units while leaving the anchor value external.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.