mesonSpectrumCert
plain-language theorem explainer
mesonSpectrumCert packages the five-family count, constant phi mass ratio, and mass positivity into the MesonSpectrumCert structure for the phi-ladder meson spectrum. Particle physicists modeling mesons via Recognition Science would cite it to confirm the spectrum matches the predicted five canonical families. The definition is a direct substitution that populates the structure fields from the three supporting theorems.
Claim. The meson spectrum certificate is the structure asserting that the set of meson families has cardinality 5, that the mass ratio between adjacent families on the golden-ratio ladder equals the golden ratio phi, and that every meson mass is strictly positive.
background
The module constructs the meson spectrum on the phi-ladder with five families: pseudoscalar (pi, K, eta), vector (rho, omega, K*, phi), scalar (a0, f0), axial vector (a1, b1), and tensor (a2, f2). Adjacent families differ by the golden ratio in mass. The structure MesonSpectrumCert requires three properties: the family count equals 5, the mass ratio mesonMass(k+1)/mesonMass(k) = phi for all k, and mesonMass(k) > 0 for all k. Upstream results include the theorem mesonFamily_count proving the cardinality by decision, mass_ratio proving the ratio via unfolding and ring simplification, and mass_pos proving positivity from pow_pos.
proof idea
The definition is a one-line wrapper that directly assigns the theorem mesonFamily_count to the five_families field, the theorem mass_ratio to the phi_ratio field, and the theorem mass_pos to the mass_always_pos field of the MesonSpectrumCert structure.
why it matters
This definition supplies the certified meson spectrum that aligns with the phi-ladder mass formula in Recognition Science. It completes the local construction in the MesonSpectrumFromPhiLadder module, providing a concrete instance for the five-family spectrum with phi ratios. The certificate supports the framework's mass formula yardstick times phi to the (rung minus 8 plus gap) on the phi-ladder and is consistent with the eight-tick octave and D=3 from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.