ell0_pos
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute any numerical value for ℓ₀.
- Does not prove the positivity of c_codata or τ₀.
- Does not address unit conversions to SI or other systems.
- Does not extend the result to signed or complex lengths.
Lean usage
lemma ell0_ne_zero : ell0 ≠ 0 := ne_of_gt ell0_posformal statement (Lean)
73lemma ell0_pos : 0 < ell0 := mul_pos c_codata_pos tau0_pos