c_codata_pos
plain-language theorem explainer
The lemma asserts that the codata speed of light is strictly positive. Researchers deriving Planck units and other constants from Recognition Science primitives cite this result to guarantee positivity of downstream expressions. The proof is a direct one-line wrapper that unfolds the definition and applies numerical normalization.
Claim. $0 < c$ where $c = 299792458$ is the CODATA reference value for the speed of light in meters per second.
background
The Constants.Derivation module adopts CODATA reference values as starting points for deriving physical constants within the Recognition Science framework. The definition c_codata fixes the speed of light at its exact SI value of 299792458. This positivity result is invoked by later lemmas that construct quantities such as the Planck length and mass, which require the inequality to hold for the square-root expressions to be well-defined and positive.
proof idea
One-line wrapper that unfolds c_codata to the literal integer 299792458 and invokes norm_num to discharge the numerical inequality.
why it matters
The lemma supplies the positivity foundation used by c_codata_ne_zero, c_derived_pos, ell0_pos, planck_length_pos and planck_mass_pos. It anchors the constants derivation step that converts CODATA inputs into RS-native expressions while preserving the sign properties needed for physical quantities. The result sits inside the broader program of obtaining c, ħ and G from the J-cost and phi-ladder primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.