l0_pos
plain-language theorem explainer
The lemma establishes that the fundamental length scale ℓ₀ is strictly positive. Researchers deriving energy scales or UV cutoffs from the Recognition constants would cite this result to justify subsequent inequalities. The proof is a one-line term reduction that unfolds the definition ℓ₀ = 1 and applies the standard fact 0 < 1 in the reals.
Claim. $0 < ℓ_0$ where $ℓ_0$ denotes the fundamental length scale.
background
The Compat.Constants module supplies project-wide constants and minimal structural lemmas. Its definition sets ℓ₀ := 1 in native units. Upstream results include the abstract Constants structure from CPM.LawOfExistence (with nonnegativity on Knet) and the QFT.UVCutoff redefinition ℓ₀ = c · τ₀ that ties the placeholder to physical scales such as E₀ = ℏ / τ₀.
proof idea
One-line term proof that unfolds the definition of l0 and invokes zero_lt_one on the reals.
why it matters
This basic positivity lemma anchors the length scale that enters mass formulas, energy scales, and the phi-ladder constructions in the Recognition framework. It supports downstream use of the eight-tick octave and D = 3 by guaranteeing a positive base length. Although currently unreferenced, it closes the minimal interface required for the compat layer to feed constants into RSBridge and Fermion structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.