MesonFamily
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute explicit masses for individual mesons.
- Does not establish the phi-ladder mass ratio property.
- Does not connect to the full forcing chain T0-T8.
- Does not address spatial dimensions D=3.
formal statement (Lean)
19inductive MesonFamily where
20 | pseudoscalar
21 | vector
22 | scalar
23 | axialVector
24 | tensor
25 deriving DecidableEq, Repr, BEq, Fintype
26