mass_ratio
plain-language theorem explainer
The theorem establishes that successive meson masses on the phi-ladder obey m(k+1)/m(k) = phi for every natural number k. Physicists working with self-similar scaling in the meson spectrum cite this to anchor the five-family structure. The proof unfolds the power definition of mesonMass and reduces the ratio by exponent arithmetic plus ring normalization.
Claim. For every natural number $k$, the ratio of the meson mass at rung $k+1$ to the mass at rung $k$ equals $phi$, where the meson mass function is defined by $m(k) := phi^k$.
background
The Meson Spectrum from φ-ladder module treats five canonical meson families (pseudoscalar, vector, scalar, axial-vector, tensor) as configDim D = 5. The mesonMass function is the noncomputable definition mesonMass k := phi^k, placing each family on the phi-ladder. This mirrors the adjacent-eigenstate ratio theorem in NeutrinoMassFromPhiLadder, which states neutrinoMass (k+1)/neutrinoMass k = phi by the same unfolding and ring steps.
proof idea
The term proof unfolds mesonMass to obtain phi^(k+1)/phi^k. It introduces the positivity fact (0 < phi^k) via pow_pos, rewrites the division equation with div_eq_iff, replaces the successor exponent with pow_succ, and closes the equality by ring.
why it matters
This supplies the phi_ratio field inside MesonSpectrumCert, which is consumed by FermionKineticCert (for mass_ratio in the fermion structure) and by DarkMatterMassFromGap45. It realizes the self-similar fixed point phi forced at T6 of the UnifiedForcingChain and the Recognition Composition Law scaling that produces the eight-tick octave. The module doc flags the result as part of the S2 Depth certification with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.