Generation
plain-language theorem explainer
The inductive type Generation enumerates the three fermion generations as first, second and third. Mass-ratio derivations on the φ-ladder cite this enumeration to index the torsion offsets 0, 11 and 17 that arise from Q3 cube combinatorics. The definition is a direct inductive enumeration equipped with decidable equality and inhabited instances.
Claim. The fermion generations form the inductive type with three constructors: first, second, third.
background
The RSLedger module equips the φ-ladder with generation-dependent torsion so that rung numbers become baseRung + τ_g and mass ratios become φ to the difference of rungs. Torsion values are obtained from D=3 cube geometry: Gen 1 is the ground state with τ=0, Gen 2 uses passive_field_edges(D)=11, and Gen 3 adds cube_faces(D)=6 to reach τ=17. The module imports cube_faces and passive_field_edges from AlphaDerivation and PlanckScaleMatching; upstream LedgerFactorization.of supplies the underlying (ℝ₊, ×) structure while NucleosynthesisTiers.of places nuclear densities on the same φ-tiers.
proof idea
The declaration is an inductive definition that directly introduces the three constructors together with deriving clauses for DecidableEq, Repr and Inhabited. No lemmas or tactics are invoked.
why it matters
This definition supplies the discrete labels required by the three_generations_from_dimension theorem, which shows that D=3 forces exactly three generations via the face-pair count of the cube. It is also used by gauge_generators_eq_edges and closure_populates_next to index ledger composition steps. Within the Recognition framework it realizes the T8 step that fixes D=3 and thereby fixes the fermion spectrum; the open question it touches is whether modified torsion rules could admit a fourth generation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.