HadronFamily
HadronFamily enumerates the five canonical hadron families (pion, kaon, eta, rho, omega) that RS equates with configuration dimension D at spatial dimension 3. Researchers mapping Gell-Mann's eight-fold way to the 2^D lattice period cite this when counting families against the T7 eight-tick octave. The declaration is a direct inductive definition that derives Fintype, enabling the cardinality to be settled by decide.
claimLet $H$ be the inductive type whose constructors are the pion, kaon, eta, rho, and omega families, equipped with decidable equality, representation, Boolean equality, and finite-type structure.
background
The module derives the eight-fold way from Recognition Science by identifying 8 with the 2^D lattice period at D=3 and 10 with 2 times 5. Five canonical hadron families are set equal to configDim D. The upstream eta from Nucleosynthesis is the baryon-to-photon ratio 6.1e-10 that enters BBN reaction chains, while the eta from Metric is the bilinear form that returns -1 or +1 on the diagonal according to index parity.
proof idea
The declaration is an inductive definition that lists the five families explicitly and derives the Fintype instance by the standard Mathlib mechanism, so that cardinality computation reduces to decide.
why it matters in Recognition Science
HadronFamily supplies the five_families field of the EightFoldWayCert structure and is the target of the hadronFamilyCount theorem. It completes the RS account of the eight-fold way by fixing the number of families at configDim D=5, consistent with the T7 eight-tick octave and the D=3 spatial dimensions forced by the unified chain.
scope and limits
- Does not derive masses or decay widths of the listed families.
- Does not reconstruct SU(3) representations from the J-cost or RCL.
- Does not address quark substructure or confinement dynamics.
- Does not connect the families to the phi-ladder mass formula.
formal statement (Lean)
33inductive HadronFamily where
34 | pion | kaon | eta | rho | omega
35 deriving DecidableEq, Repr, BEq, Fintype
36