ell0_ne_zero
The lemma confirms that the fundamental length scale ell0 remains nonzero in the Recognition Science codata unit system. Derivations of constants such as Planck units or voxel scales cite it to guarantee that divisions and inverses involving ell0 are well-defined. The proof is a direct term application of the standard fact that every positive real is nonzero.
claim$ell_0 neq 0$, where $ell_0 := c_{rm codata} cdot tau_0$ is the fundamental length constructed from the CODATA speed of light and the derived time scale $tau_0$.
background
The Constants.Derivation module derives physical constants from Recognition Science primitives by matching CODATA reference values for $c$, $hbar$, and $G$. The length scale is introduced by the definition $ell_0 := c_{rm codata} cdot tau_0$, where $tau_0$ satisfies the upstream identity $tau_0^2 = hbar_{rm codata} G_{rm codata} / (pi c_{rm codata}^5)$. The sibling lemma ell0_pos supplies the positivity fact $0 < ell_0$ via multiplication of the positive terms $c_{rm codata pos}$ and $tau_0 pos$.
proof idea
The proof is a one-line term wrapper that applies ne_of_gt directly to the positivity lemma ell0_pos. No unfolding, case analysis, or additional lemmas are required.
why it matters in Recognition Science
The result secures the invertibility of the base length in the RS unit system, supporting the codata embeddings of $c$, $hbar$, and $G$ that feed the mass formula and alpha-band calculations. It aligns with the T0-T8 forcing chain by preserving the nondegeneracy of the voxel scale before the phi-ladder is imposed. No downstream theorems currently invoke it, leaving its use in later constant derivations open.
scope and limits
- Does not prove positivity of ell0 (relies on the separate ell0_pos lemma).
- Does not compute or bound the numerical value of ell0.
- Does not connect ell0 to the J-function or phi-ladder mass formula.
- Does not address dimensional analysis beyond the codata definition.
formal statement (Lean)
74lemma ell0_ne_zero : ell0 ≠ 0 := ne_of_gt ell0_pos
proof body
Term-mode proof.
75
76/-! ## RS Unit System Structure -/
77