genOf

formal source

 143/-! ### Generation indexing (three disjoint families) -/
 144
 145/-- Generation index (0,1,2) assigned by rung/sector ordering. -/
 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. -/
 153theorem genOf_surjective : Function.Surjective genOf := by
 154  intro i
 155  have h : i.val = 0 ∨ i.val = 1 ∨ i.val = 2 := by
 156    fin_cases i <;> simp
 157  rcases h with h0 | h12
 158  · -- i = 0
 159    refine ⟨Fermion.e, ?_⟩
 160    apply Fin.ext
 161    simp [genOf, h0]
 162  · rcases h12 with h1 | h2
 163    · -- i = 1
 164      refine ⟨Fermion.mu, ?_⟩
 165      apply Fin.ext
 166      simp [genOf, h1]
 167    · -- i = 2
 168      refine ⟨Fermion.tau, ?_⟩
 169      apply Fin.ext
 170      simp [genOf, h2]
 171
 172/-! ### Admissible family encoding via rung residue classes and equal‑Z -/
 173
 174/-- Rung residue class modulo 360 (the joint sync scale of 8‑beat and rung‑45). -/
 175def rungResidueClass (a : ℤ) : Set Fermion :=
 176  { f | Int.ModEq (360 : ℤ) (rung f) a }