normalForm

formal source

  71      if cancels a b then rest else a :: rewriteOnce (b :: rest)
  72
  73/-- Normalization via bounded passes: at most length passes strictly reduce on success. -/
  74def normalForm (w : Word) : Word :=
  75  let rec normalize (current : Word) (passes : Nat) : Word :=
  76    if passes = 0 then current
  77    else
  78      let next := rewriteOnce current
  79      if next.length = current.length then current
  80      else normalize next (passes - 1)
  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**