Generation
plain-language theorem explainer
The framework fixes the set of fermion generations to a three-element finite type to match the face-pair count of the three-dimensional cube. Particle physicists working within Recognition Science would cite this when counting chiral states or deriving the Standard Model spectrum from Q3 geometry. The declaration is a direct abbreviation to the standard finite type of cardinality three.
Claim. The set of particle generations is the finite type with exactly three elements, written $G = {0,1,2}$.
background
The Spectral Emergence module starts from the forced datum D=3 and shows that the binary cube Q3 simultaneously produces the gauge group SU(3)×SU(2)×U(1), exactly three generations via face-pair counting, and 48 chiral fermion states equal to |Aut(Q3)|. Upstream results in other modules introduce Generation either as a plain Nat or as an inductive type with constructors first, second, third; the present abbreviation specializes the type for direct combinatorial use inside this module. The module document emphasizes that all such counts follow from elementary algebra on the constant phi with zero free parameters.
proof idea
One-line definition that sets the generation type to the standard finite set of cardinality three.
why it matters
This abbreviation supplies the type used in the parent theorem three_generations_from_dimension, which resolves the P-001 claim that three generations follow from D=3 via face pairs. It also appears in the gauge-order product that recovers |Aut(Q3)|=48 and in ledger composition results that populate the phi-ladder. The definition therefore closes the link from the T8 dimension-forcing step through the eight-tick octave to the observed three-family structure of the Standard Model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.