ell

formal source

  81  normalize w w.length
  82
  83/-- Reduced length ℓ(W) as length of the normal form. -/
  84@[simp] def ell (w : Word) : Nat := (normalForm w).length
  85
  86/-- Net winding on the eight‑tick clock (abstracted): +1 for dir, −1 otherwise. -/
  87noncomputable def winding (w : Word) : Int :=
  88  (w.map (fun r => if r.dir then (1 : Int) else (-1 : Int))).foldl (·+·) 0
  89
  90/-- Formal torsion mod‑8 class wrapper. -/
  91-- Proper mod‑8 torsion quotient.
  92abbrev Torsion8 := ZMod 8
  93
  94/-- Torsion class via ZMod 8. -/
  95@[simp] noncomputable def torsion8 (w : Word) : Torsion8 := (winding w : Int) -- coerces into ZMod 8
  96
  97/-- Map mod-8 torsion to a 3-class generation label. -/
  98@[simp] noncomputable def genOfTorsion (t : Torsion8) : Derivation.GenClass :=
  99  match (t.val % 3) with
 100  | 0 => Derivation.GenClass.g1
 101  | 1 => Derivation.GenClass.g2
 102  | _ => Derivation.GenClass.g3
 103
 104/-- **LEPTON RUNG DERIVATION**
 105    The charged lepton rungs {2, 13, 19} are derived from the reduced length ℓ
 106    and the generation torsion τ_g.
 107
 108    ℓ = 2 (minimal neutral loop)
 109    τ_g ∈ {0, 11, 17} for generations {1, 2, 3}
 110
 111    r = ℓ + τ_g
 112    Generation 1 (e):   2 + 0 = 2
 113    Generation 2 (mu):  2 + 11 = 13
 114    Generation 3 (tau): 2 + 17 = 19 -/