genOf_surjective
plain-language theorem explainer
The generation assignment from the twelve standard-model fermions onto the three-element index set is surjective. A particle physicist bounding family replication or sterile states would cite the result to fix the number of generations at three. The argument proceeds by exhaustive case analysis on the target index, exhibiting the electron, muon, and tau lepton in turn.
Claim. Let $genOf$ map each fermion species to its generation label in the three-element set. Then $genOf$ is surjective.
background
The RSBridge.Anchor module encodes the twelve standard-model fermions together with the charge-indexed integer $Z_i = q̃² + q̃⁴$ (plus four for quarks) and the gap function $F(Z) = ln(1 + Z/φ)/ln(φ)$. This gap supplies the closed-form residue that the integrated renormalization-group flow from the anchor scale is required to match at tolerance ~10^{-6}. The local setting is single-anchor phenomenology, in which family mass ratios for equal-$Z$ species reduce to pure powers of φ.
proof idea
The proof performs case analysis on the target index $i$ in the three-element set via fin_cases. For each value it selects the corresponding charged lepton (electron for 0, muon for 1, tau for 2) and applies Fin.ext together with simplification to confirm that the generation label matches the index.
why it matters
The result supplies the surjectivity hypothesis required by the sterile-exclusion theorem that rules out a fourth generation. It fills the enumeration step in the RSBridge anchor construction, consistent with the eight-tick octave and the phi-ladder mass formula. The theorem closes the charged-lepton family count at the anchor scale and supports downstream claims that no additional rung or tau_g exists without violating minimality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.