ell0_pos
plain-language theorem explainer
Positivity of the fundamental length ℓ₀ follows directly from the positivity of its defining factors c_codata and τ₀. Researchers constructing RS-native unit systems or proving entropy bounds cite this result to guarantee strictly positive lengths. The proof is a one-line wrapper applying the mul_pos lemma to the two upstream positivity statements.
Claim. Let $c > 0$ and $0 < τ_0$. Define the fundamental length by $ℓ_0 := c · τ_0$. Then $ℓ_0 > 0$.
background
The module derives physical constants from Recognition Science primitives, referencing CODATA values for c, ℏ and G. The fundamental length ℓ₀ is the RS-native voxel length defined by the light-cone identity ℓ₀ = c_codata · τ₀. Upstream, tau0_pos establishes 0 < τ₀ by simplification to 0 < 1, c_codata_pos follows from norm_num on the codata definition, and ell0 itself is introduced as the product in the Derivation submodule.
proof idea
The proof is a one-line wrapper that invokes mul_pos on c_codata_pos and tau0_pos.
why it matters
This positivity result supplies the ℓ_pos field for the canonicalUnits RSUnitSystem definition and is invoked by ell0_ne_zero. It supports downstream theorems on RS entropy positivity and the coupling lock-in condition at the ell0 scale. It completes the basic positivity infrastructure required by the constants derivation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.