c_ne_zero
plain-language theorem explainer
The lemma asserts that the speed of light c is nonzero in RS-native units. Any derivation requiring inversion of c or division by c would cite it to clear the denominator. The proof is a one-line wrapper that applies the library rule ne_of_gt to the upstream positivity statement c > 0.
Claim. In RS-native units the speed of light satisfies $c ≠ 0$.
background
The Codata module quarantines empirical SI/CODATA constants (c, ħ, G) from the certified surface so that the main forcing-chain certificate never depends on numeric values. The constant c is defined here as the speed of light expressed in voxel-per-tick units. Three upstream lemmas each establish the strict inequality 0 < c, either by direct simplification of the definition or by reduction to the RS-native value 1.
proof idea
The proof is a one-line wrapper that applies the Mathlib lemma ne_of_gt to the hypothesis c_pos.
why it matters
It supplies the elementary non-vanishing fact needed whenever c appears in a denominator inside the quarantined constants module. The module design keeps these empirical values separate from the core Recognition Science derivations that begin from the forcing chain T0-T8 and the Recognition Composition Law. No downstream theorem in the current graph depends on this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.