c_codata_ne_zero
plain-language theorem explainer
Physicists deriving relations between Planck units and recognition primitives cite this lemma to justify divisions by c in expressions for tau0. It asserts that the exact SI value 299792458 is nonzero. The proof is a direct one-line application of ne_of_gt to the already-proved positivity of the same constant.
Claim. $c_{codata} = 299792458$ satisfies $c_{codata} ≠ 0$.
background
The module derives physical constants from Recognition Science primitives using CODATA reference values for c, ℏ and G. c_codata is defined as the exact SI value 299792458. The upstream positivity lemma states 0 < c_codata by direct numerical evaluation after unfolding the definition.
proof idea
One-line wrapper that applies ne_of_gt to c_codata_pos.
why it matters
This lemma is invoked in G_relation_satisfied, planck_relation_satisfied, tau0_planck_relation and tau0_sq_eq to discharge the nonzero hypotheses required for algebraic manipulations of tau0. Those theorems in turn confirm consistency between derived constants and the CODATA values used in the Recognition forcing chain. It touches the open question of how the exact SI value of c emerges from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.