MesonFamily
plain-language theorem explainer
The MesonFamily inductive type enumerates the five canonical meson families in the Recognition Science phi-ladder model for hadron spectra. Researchers modeling meson masses via self-similar ratios would reference this enumeration to establish the configuration dimension D equals 5. The definition consists of five constructors and automatically derives Fintype for cardinality calculations.
Claim. The set of meson families is the inductive type consisting of the five elements pseudoscalar, vector, scalar, axial-vector, and tensor.
background
The module establishes the meson spectrum from the phi-ladder at S2 depth. It identifies five canonical families corresponding to configuration dimension D = 5: pseudoscalar mesons such as π, K, η; vector mesons such as ρ, ω, K*, φ; scalar mesons a₀, f₀; axial vector mesons a₁, b₁; and tensor mesons a₂, f₂. This enumeration supports the adjacent-family mass ratio property on the phi-ladder.
proof idea
The declaration is an inductive definition introducing five constructors for the meson families. It derives DecidableEq, Repr, BEq, and Fintype to support equality checks and finite cardinality computations.
why it matters
This definition supplies the five families required by the MesonSpectrumCert structure, which asserts Fintype.card MesonFamily = 5 together with the phi ratio and positive mass conditions. It anchors the Recognition Science treatment of meson spectra within the phi-ladder framework, where the five families realize the configuration dimension D = 5 and enable derivation of mass ratios via the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.