genOf_surjective
plain-language theorem explainer
The generation index map from Fin 3 to the three charged leptons is surjective. Extensions of the Standard Model cite this to exclude a fourth generation on minimality grounds. The proof exhausts the three cases of the finite index via fin_cases and explicit preimage construction.
Claim. The map sending each index $i$ in the three-element set to the corresponding charged lepton (electron for 0, muon for 1, tau for 2) is surjective.
background
The RSBridge.Anchor module encodes the twelve Standard Model fermions as the Fermion type and defines ZOf as the charge-indexed integer together with the gap display function $F(Z) = ln(1 + Z/φ)/ln(φ)$. The generation index lives in Fin 3 and selects the three charged leptons as representatives. This sits inside the single-anchor phenomenology where the integrated RG residue equals gap(ZOf i) at the anchor scale μ⋆ with tolerance ~1e-6.
proof idea
The proof opens with intro i, then applies fin_cases on i to obtain the disjunction i.val = 0 ∨ 1 ∨ 2. Each disjunct is handled by rcases, after which refine supplies the explicit preimage (Fermion.e, Fermion.mu or Fermion.tau) and Fin.ext together with simp closes the equality.
why it matters
This theorem supplies the exact count of three generations required by the downstream no_sterile result in Physics.SterileExclusion, which derives a contradiction for any hypothetical fourth generation. It fills the minimality step in the RSBridge anchor construction and is consistent with the eight-tick octave (T7) and D = 3 spatial dimensions (T8) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.