genOf
plain-language theorem explainer
The generation index function assigns each of the twelve Standard Model fermions to an integer in {0,1,2} by rung and sector ordering. Researchers building fermion mass ladders or rung numbers within Recognition Science cite this map when evaluating phi-powers on the mass formula. It is realized by exhaustive case analysis on the Fermion inductive type that sends first-generation species to 0, second-generation species to 1, and third-generation species to 2.
Claim. Let $F$ be the set of Standard Model fermions (six quarks, three charged leptons, three neutrinos). The map $g:F→{0,1,2}$ sends $e,u,d,ν_1$ to 0, $μ,c,s,ν_2$ to 1, and $τ,t,b,ν_3$ to 2.
background
This definition sits inside the RSBridge.Anchor module, which supplies the bridge from the recognition framework to particle physics. The module introduces the Fermion inductive type, the charge-indexed integer ZOf, the gap function F(Z)=ln(1+Z/φ)/ln(φ), and the anchor-scale mass construction. It situates these objects in RG transport, where the integrated residue at the anchor equals the gap function with tolerance ~1e-6.
proof idea
The definition is a direct pattern match on the twelve constructors of the Fermion inductive type. Each arm returns the corresponding element of Fin 3 together with a decidable proof. No external lemmas are applied; the construction is purely definitional.
why it matters
The map supplies the generation label required by the surjectivity theorem genOf_surjective and by the rung constructors compute_rung and compute_rung_sdgt. It connects the SpectralEmergence result that Q3 forces exactly three generations to the concrete mass formula yardstick·φ^(rung-8+gap(Z)). The assignment is a prerequisite for the sterile-neutrino exclusion arguments that rely on surjectivity onto Fin 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.