generationTypeCount
plain-language theorem explainer
The theorem asserts that the finite type of fermion generations has cardinality exactly three. Recognition Science researchers cite it to match the Standard Model's three generations to spatial dimension D via cube geometry. The proof is a one-line decide tactic that enumerates the three constructors of the inductive type.
Claim. $|FermionGeneration| = 3$, where FermionGeneration is the inductive type whose constructors are first, second, and third.
background
The module shows that the Standard Model has three generations of fermions because RS equates three generations to D = 3 spatial dimensions, which equals the number of cube face-pairs. Each generation contains four fermions (up, down, charged lepton, neutrino), so three generations yield twelve Weyl fermions matching the twelve cube edges. The key definition is the inductive type FermionGeneration with constructors first, second, third that derives a Fintype instance for direct cardinality computation. This depends on the upstream inductive definition of FermionGeneration.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes Fintype.card by enumerating the three constructors of FermionGeneration and confirms the result equals 3.
why it matters
It supplies the generation_types field inside the GenerationCert definition, which certifies three generations equal D together with the total fermion count of 12 and the cube-edge match. This fills the A1 SM Depth claim that three generations equal D from the Recognition Science framework, specifically tying to T8 where D = 3 arises from the eight-tick octave and cube face-pairs. No open questions remain in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.