MesonSpectrumCert
plain-language theorem explainer
The MesonSpectrumCert structure encodes that the meson spectrum comprises exactly five families whose masses form a geometric sequence with common ratio phi. A physicist constructing effective hadron models from self-similar ladders would cite it to fix the family count and enforce the scaling. The declaration is a plain record whose fields are satisfied by the cardinality of the MesonFamily inductive type and the explicit exponential definition of mesonMass.
Claim. Let $m(k) := phi^k$ for $k in mathbb{N}$ and let $phi$ be the golden ratio. A MesonSpectrumCert is a record asserting that the set of meson families has cardinality five, that $m(k+1)/m(k) = phi$ for every natural number $k$, and that $m(k) > 0$ for every $k$.
background
The module defines the phi-ladder model for mesons. MesonFamily is the inductive type with five constructors: pseudoscalar, vector, scalar, axialVector, and tensor. The auxiliary function mesonMass is defined by mesonMass k := phi ^ k. The golden ratio phi is taken from Constants, and the adjacent ratio property is the same scaling that appears in the upstream phi_ratio definition from the Quasicrystal module.
proof idea
The structure is declared directly as a record type. Its three fields are the cardinality statement, the universal ratio equation, and the positivity predicate. No tactics or lemmas are invoked inside the declaration; the fields are later instantiated by the sibling definitions mesonFamily_count, mass_ratio, and mass_pos inside the downstream mesonSpectrumCert constructor.
why it matters
MesonSpectrumCert supplies the data record consumed by mesonSpectrumCert, which in turn provides the explicit five-family phi-ladder spectrum used in the Recognition mass formula. It realizes the configDim = 5 assignment for the meson sector and connects to the self-similar fixed point (T6) together with the phi-ladder rung scaling. The declaration closes the concrete spectrum construction inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.