planck_length_pos
plain-language theorem explainer
The lemma establishes positivity of the Planck length constructed from CODATA-anchored constants in the Recognition Science constants module. Researchers verifying length scales on the phi-ladder would cite it to guarantee the square-root expression is defined over the reals. The proof is a direct term-mode application of sqrt_pos after unfolding the definition and chaining mul_pos, div_pos, and pow_pos on the three positive codata quantities.
Claim. $0 < sqrt( hbar_codata * G_codata / c_codata^3 )$
background
The Constants.Derivation module anchors derived constants to CODATA reference values: c = 299792458 m/s, ℏ = 1.054571817×10⁻³⁴ J·s, G = 6.67430×10⁻¹¹ m³/(kg·s²). Planck length is introduced by the definition sqrt(hbar_codata * G_codata / c_codata^3). Three upstream lemmas establish that c_codata, hbar_codata, and G_codata are each strictly positive by unfolding to numeric literals and applying norm_num.
proof idea
Unfold the definition of planck_length to expose the radicand. Apply sqrt_pos.mpr to the claim that the argument is positive. The radicand positivity follows from mul_pos on the two positive factors hbar_codata and G_codata, then div_pos by the positive quantity c_codata^3 obtained via pow_pos.
why it matters
The result supplies a basic positivity guarantee for the Planck length inside the constants derivation that feeds the Recognition Science framework. It supports any later use of length scales in mass formulas or dimensional relations by ensuring the square root remains real and positive. The lemma closes a routine check that would otherwise block downstream applications of the G_relation_satisfied theorem and similar codata identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.