pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

Generation

show as:
view Lean formalization →

Generation is defined as the finite set with three elements. Researchers deriving the Standard Model from the Recognition Science forcing chain cite this as the explicit index type for the three fermion generations. The definition is a direct one-line abbreviation of the standard three-element finite type that encodes D = 3 into the generation count.

claimThe set of fermion generations is the finite set with three elements, denoted $G = {0,1,2}$.

background

The Spectral Emergence module starts from the forced datum D = 3 (T8) that produces the binary cube Q₃ with eight vertices. The module documentation states that this geometry simultaneously forces SU(3) × SU(2) × U(1) gauge content, exactly three particle generations from face-pair count, and 24 chiral fermion flavors. Upstream results supply related but distinct Generation types: an inductive enumeration in Physics.ThreeGenerations that labels modes by parity patterns across dimensions, and a similar inductive type in RecogSpec.RSLedger that records first, second, and third generations with torsion from Q₃ geometry.

proof idea

The declaration is a direct abbreviation of the standard finite type with three elements. No lemmas or tactics are invoked; the abbreviation simply supplies a concrete index set for the three generations required by the cube face-pair counting.

why it matters in Recognition Science

This supplies the generation type used by three_generations_from_dimension, which resolves P-001 by proving face_pairs D_physical = 3, and by gauge_generators_eq_edges that equates total gauge rank to the edge count of Q₃. It closes the loop from T8 (D = 3) through the eight-tick octave and phi-ladder to the explicit count of three generations, as the module records: '3 face pairs → 3 generations'. The definition touches the open question of whether any D ≠ 3 can satisfy the full list of requirements listed in the module documentation.

scope and limits

formal statement (Lean)

 207abbrev Generation := Fin 3

proof body

Definition body.

 208
 209/-- **THEOREM**: The generation count matches the cube dimension. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.