hadronFamilyCount
The theorem establishes that the finite type enumerating the five canonical hadron families has cardinality exactly five. Particle physicists and Recognition Science modelers would cite this when linking the spatial dimension D=3 to the count of meson and baryon families in the eight-fold way. The proof is a direct decision procedure that evaluates the Fintype instance on the inductive type definition.
claimThe cardinality of the finite type of hadron families is five: $|H| = 5$, where $H$ is the set consisting of the five elements pion, kaon, eta, rho, and omega.
background
The Eight-Fold Way from RS module connects Gell-Mann's classification to Recognition Science by setting octet size to 2^D with D=3 and decuplet size to 2 times 5. The HadronFamily inductive type lists the five families that correspond to configDim D = 5 in the framework. This rests on the upstream inductive definition of HadronFamily, which derives DecidableEq, Repr, BEq, and Fintype to support direct cardinality computation.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the goal Fintype.card HadronFamily = 5. The tactic succeeds because the inductive type derives a Fintype instance that enumerates the five constructors and returns their count.
why it matters in Recognition Science
This supplies the five_families field inside the EightFoldWayCert definition, completing the Lean certification of the eight-fold way from RS. It instantiates the T7 eight-tick octave and T8 D=3 landmarks by fixing the family count at configDim D = 5, consistent with the module's zero-sorry status for these structural counts.
scope and limits
- Does not derive masses or decay rates for the families.
- Does not address interactions or quantum numbers within families.
- Does not extend the count to higher dimensions or additional families.
- Does not prove empirical existence of these particles.
Lean usage
def cert : EightFoldWayCert := { octet_2cubeD := mesonOctet_eq_2cubeD, decuplet_2times5 := decuplet_eq_2_times_5, five_families := hadronFamilyCount }formal statement (Lean)
37theorem hadronFamilyCount : Fintype.card HadronFamily = 5 := by decide
proof body
38