c_codata
plain-language theorem explainer
The definition supplies the exact numerical value of the speed of light from the SI definition as 299792458 meters per second. Derivations of other constants such as the derived gravitational constant and the base length ell0 cite it to equate their Recognition Science expressions to physical measurements. It is introduced as a plain real number constant without further computation or proof.
Claim. Let $c$ denote the speed of light. Then $c = 299792458$ in meters per second, as fixed by the SI definition.
background
This module derives physical constants from Recognition Science primitives while anchoring them to CODATA reference values. The speed of light is taken as the exact SI value of 299792458 m/s. Other constants like ℏ and G are similarly referenced for use in derivations such as the relation for tau0 squared equaling ℏG/(πc^5). The local setting is the derivation of constants like ell0 = c * tau0 from the primitives.
proof idea
The declaration is a direct definition assigning the integer value 299792458 to the real number constant representing the speed of light.
why it matters
This anchors theorems such as c_derived_eq_codata, which equates the RS-derived speed of light to this value under unit system consistency, and G_relation_satisfied, which confirms the gravitational constant matches CODATA. It connects the Recognition Science framework to physical measurements, with c set to 1 in native units but here using the exact experimental value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.