genOf
The genOf definition maps each of the twelve Standard Model fermions to a generation index in {0,1,2} according to the rung and sector ordering of the Recognition Science bridge. Mass-ladder constructors and sterile-neutrino exclusion arguments cite this assignment when determining phi-ladder positions or proving that no fourth generation fits inside Fin 3. The definition is realized by exhaustive pattern matching on the Fermion inductive type with explicit Fin 3 literals.
claimThe generation index function sends each fermion species to an element of $Fin 3$ by the rule that first-generation species (electron, up quark, down quark, first neutrino) receive index 0, second-generation species receive index 1, and third-generation species receive index 2.
background
The Fermion inductive type enumerates the twelve Standard Model fermions via the constructors d, s, b, u, c, t, e, mu, tau, nu1, nu2, nu3. In the RSBridge.Anchor module this type supplies the interface between the recognition framework and particle phenomenology, connecting to the ZOf charge index and the gap function F(Z) = ln(1 + Z/φ)/ln(φ) that fixes mass ratios at the anchor scale μ⋆. Upstream, the SpectralEmergence structure records that exactly three generations are forced by the face-pair count of the Q3 lattice, supplying the warrant for restricting the codomain to Fin 3.
proof idea
The definition proceeds by direct case analysis on the twelve constructors of the Fermion inductive type, with each constructor mapped to the appropriate element of Fin 3 via explicit literals and decide tactics that discharge the Fin bounds.
why it matters in Recognition Science
This assignment is invoked by the rung constructors compute_rung and compute_rung_sdgt to locate each species on the phi-ladder, and it supplies the hypothesis for the surjectivity theorem genOf_surjective that establishes exactly three generations. The same map appears in the sterile-exclusion theorems genOf_hyp, no_sterile and sterile_bound, where surjectivity onto Fin 3 precludes a fourth generation. The construction therefore realizes the three-generation prediction of the SpectralEmergence structure inside the Recognition Science forcing chain.
scope and limits
- Does not compute physical masses or rung numbers.
- Does not define the gap function or ZOf index.
- Does not prove surjectivity or any other property of the map.
- Does not extend the domain to hypothetical or sterile fermions.
Lean usage
def compute_rung (f : Fermion) : ℤ := let sector := sectorOf (.fermion f); let gen := (genOf f).val; ...formal statement (Lean)
146def genOf : Fermion → Fin 3
147| .e => ⟨0, by decide⟩ | .mu => ⟨1, by decide⟩ | .tau => ⟨2, by decide⟩
148| .u => ⟨0, by decide⟩ | .c => ⟨1, by decide⟩ | .t => ⟨2, by decide⟩
149| .d => ⟨0, by decide⟩ | .s => ⟨1, by decide⟩ | .b => ⟨2, by decide⟩
150| .nu1 => ⟨0, by decide⟩ | .nu2 => ⟨1, by decide⟩ | .nu3 => ⟨2, by decide⟩
151
152/-- Surjectivity of the generation index: there are exactly three generations. -/