ell0_ne_zero
plain-language theorem explainer
The lemma shows that the RS-native fundamental length ℓ₀ is nonzero. Researchers deriving constants from the phi-ladder and forcing chain cite it to keep denominators valid in mass and time expressions. The proof is a one-line term application of the fact that a positive real cannot be zero.
Claim. $ℓ_0 ≠ 0$, where $ℓ_0 := c_{codata} · τ_0$ is the product of the codata speed of light and the fundamental time interval.
background
In Constants.Derivation the fundamental length is introduced as the product $ℓ_0 := c_{codata} · τ_0$. The sibling lemma ell0_pos already records that this product is strictly positive by multiplying the two positive factors c_codata_pos and tau0_pos. The module sits inside the larger derivation of CODATA values from Recognition Science primitives, with imports from CrystalStructure and BoltzmannDistribution that are not invoked here.
proof idea
Term-mode one-liner that applies ne_of_gt directly to the positivity lemma ell0_pos.
why it matters
The result supplies a basic nonzeroness guard inside the constants derivation. It supports the phi-ladder mass formula and the expression for τ₀² = ℏG/(πc⁵) by ensuring ℓ₀ never vanishes in denominators. It aligns with the T5 J-uniqueness and T8 requirement of three spatial dimensions by keeping the native length and time units well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.