IndisputableMonolith.Physics.MesonSpectrumFromPhiLadder
Defines meson families and their masses on the Recognition Science phi-ladder, with positivity and ratio lemmas plus a spectrum certificate. Particle physicists matching light-meson mass ratios to the golden-ratio ladder would cite it. The module is mostly definitions and elementary positivity/ratio facts over the rung formula, not a deep derivation.
claimMeson families are assigned discrete rungs on the $\varphi$-ladder; each meson mass is of the form $m = y\,\varphi^{r-8+g}$ (yardstick $y$, rung $r$, gap $g$), with $m>0$ and explicit mass ratios $m_i/m_j=\varphi^{\Delta r}$. A certificate packages the family count and spectrum data.
background
Recognition Science places particle masses on a discrete $\varphi$-ladder: $m = y,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$, with $\varphi$ the unique self-similar fixed point forced at T6 and $y$ a sector yardstick. The eight-tick octave (T7) and $D=3$ (T8) fix the combinatorial scaffolding; here only the ladder arithmetic is used.
This module sits in the Physics domain and imports only Constants (RS-native units, including the tick $\tau_0$). It introduces an enumeration of meson families, a count, a mass map mesonMass, ratio and positivity lemmas, and a bundled MesonSpectrumCert. No continuum QCD input appears; masses are pure ladder exponents.
proof idea
Definition module with thin lemmas. Families and the mass function are data. Positivity follows from $\varphi>1$ and positive yardstick. Mass ratios collapse to pure powers of $\varphi$ by cancelling the common yardstick and gap offset. The certificate is a structure packing the count and spectrum facts; no heavy tactic proof or external analytic input.
why it matters in Recognition Science
Supplies the meson-side instance of the RS mass formula so spectrum tables and ratio checks can be stated inside Lean. Downstream use is not yet wired in this graph (used_by empty), but the certificate pattern matches other RS particle-sector certs that feed global consistency reports. Ties directly to the phi-ladder mass formula and T6 forcing of $\varphi$; does not itself touch RCL, alpha, or the forcing chain T0–T5/T7–T8.
scope and limits
- Does not derive meson masses from QCD or lattice data.
- Does not fix yardstick or gap values from first principles here.
- Does not claim agreement with PDG beyond the ladder ansatz.
- Does not treat baryons, leptons, or gauge-boson masses.
- Does not prove uniqueness of family-to-rung assignment.