planck_length_pos
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 in Recognition Science
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.
scope and limits
- Does not derive the constants from the J-function or phi-ladder primitives.
- Does not verify numerical agreement with the experimental Planck length value.
- Does not address dimensional analysis or unit consistency beyond the algebraic expression.
- Does not connect directly to the eight-tick octave or spatial dimension forcing steps.
formal statement (Lean)
154lemma planck_length_pos : 0 < planck_length := by
proof body
Term-mode proof.
155 unfold planck_length
156 exact sqrt_pos.mpr (div_pos (mul_pos hbar_codata_pos G_codata_pos) (pow_pos c_codata_pos 3))
157