FermionGeneration
plain-language theorem explainer
The inductive type enumerates the three fermion generations as first, second, and third. Physicists deriving Standard Model particle content from Recognition Science cite it to link generation count to spatial dimension D. The definition is direct, with derived instances for decidable equality and finite type that enable automatic cardinality proofs.
Claim. Let $G$ be the set of fermion generations. Then $G$ is the inductive type with three elements: first, second, and third, equipped with decidable equality and finite cardinality.
background
Recognition Science derives the Standard Model from the forcing chain ending at T8, where D equals 3 spatial dimensions, equivalently the number of cube face-pairs. The module states that three generations equal D and that each generation contains four fermions (up, down, charged lepton, neutrino), yielding twelve Weyl fermions that match cube edges. This supplies the type used by the GenerationCert structure and the generationTypeCount theorem.
proof idea
Direct inductive definition with three constructors. The deriving clause for DecidableEq, Repr, BEq, and Fintype generates the required instances automatically, so downstream cardinality statements reduce to decide.
why it matters
This definition supplies the type for GenerationCert, which asserts generationCount equals 3, totalFermions equals 12, and totalFermions equals cubeEdges. It realizes the T8 landmark that three generations equal D=3 from the eight-tick octave. The structure closes the particle content derivation with zero axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.