hadronFamilyCount
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.