mass_pos
plain-language theorem explainer
The theorem establishes strict positivity of meson masses at every rung of the phi-ladder. Researchers constructing QRFT fermion certificates or RS black-hole models would cite it to guarantee all masses remain positive before applying further ratios or entropy formulas. The proof is a direct one-line application of the power-positivity lemma to the golden-ratio base.
Claim. For every natural number $k$, the meson mass at rung $k$ defined by $m(k) = phi^k$ satisfies $0 < m(k)$.
background
The module constructs a meson spectrum by placing five canonical families on the phi-ladder, with adjacent-family mass ratios fixed by the self-similar constant phi. The supporting definition states mesonMass k := phi ^ k, supplying the explicit mass value at each integer rung. This positivity result is invoked directly by downstream structures that embed mass ladders into larger certificates.
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the known positivity of phi.
why it matters
The result feeds OptimalConfig (which requires positive r_mass for observable flux thresholds), FermionKineticCert (which demands mass_pos for every generation), and RSBH (which uses mass_pos to establish positive entropy and Hawking temperature). It anchors the phi-ladder inside the Recognition Science framework at the step where self-similar masses are introduced, consistent with the T6 fixed-point and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.