mass_pos
The theorem shows that every meson mass on the φ-ladder is strictly positive. Modelers of meson spectra and authors of positive-mass constraints in black-hole and fermion sectors cite it. The proof is a one-line wrapper applying the positivity of φ to a natural-number exponent.
claimFor every natural number $k$, the meson mass at rung $k$ defined by $m_k = phi^k$ satisfies $m_k > 0$.
background
The module places meson masses on the φ-ladder with five canonical families (pseudoscalar, vector, scalar, axial-vector, tensor). The upstream definition supplies the explicit form $mesonMass(k) = phi^k$. This supplies the mass values whose positivity is asserted here, inside the Recognition Science treatment of adjacent-family ratios fixed by φ.
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the known positivity of phi and the natural number k.
why it matters in Recognition Science
The result is invoked in fourteen downstream declarations, including the RSBH structure (positive black-hole mass), FermionKineticCert (positive fermion masses), and OptimalConfig (observability constraints). It closes the positivity requirement for the φ-ladder mass formula in the meson sector, consistent with the self-similar fixed point φ from the forcing chain.
scope and limits
- Does not assign specific meson families to particular rungs.
- Does not derive numerical values for observed meson masses.
- Does not address decay widths or mixing angles.
- Does not extend to non-integer rungs or continuous spectra.
Lean usage
theorem positive_meson (k : ℕ) : 0 < mesonMass k := mass_pos kformal statement (Lean)
37theorem mass_pos (k : ℕ) : 0 < mesonMass k := pow_pos phi_pos k
proof body
38