planck_mass_pos
plain-language theorem explainer
The lemma establishes that the Planck mass constructed from codata values of hbar, c, and G is strictly positive. Researchers deriving constants inside the Recognition Science framework cite it to confirm the mass scale is well-defined before further use. The proof is a term-mode one-liner that unfolds the definition and applies the square-root positivity rule to the product of the three positive codata lemmas divided by the positive G.
Claim. $0 < m_P$ where $m_P = sqrt( hbar_codata * c_codata / G_codata )$ and each codata quantity is the Recognition Science input drawn from the listed CODATA reference values.
background
The module derives physical constants from Recognition Science primitives. It takes the CODATA reference values c = 299792458 m/s, hbar = 1.054571817e-34 J s, and G = 6.67430e-11 m3 kg-1 s-2 as inputs named c_codata, hbar_codata, and G_codata. The Planck mass is introduced by the definition planck_mass := sqrt (hbar_codata * c_codata / G_codata). Upstream lemmas c_codata_pos, hbar_codata_pos, and G_codata_pos each assert the corresponding codata quantity is positive; these are the only dependencies.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of planck_mass, then applies sqrt_pos.mpr to the positivity of the quotient (mul_pos hbar_codata_pos c_codata_pos) / G_codata_pos, where the three positivity facts are supplied by the upstream lemmas.
why it matters
The lemma supplies the positivity check required for the Planck mass inside the constant-derivation module. It closes the local positivity obligations for the mass scale that later steps in the Recognition Science forcing chain (T5 J-uniqueness through T8 D=3) rely upon when constructing the phi-ladder mass formula. No downstream theorems are listed, indicating the result functions as a foundational guard rather than an intermediate step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.