cancels

formal source

  44@[simp] def inv (r : Ribbon) : Ribbon := { r with dir := ! r.dir, bit := - r.bit }
  45
  46/-- Cancellation predicate for adjacent syllables (tick consistency abstracted). -/
  47@[simp] def cancels (a b : Ribbon) : Bool := (b.dir = ! a.dir) && (b.bit = - a.bit) && (b.tag = a.tag)
  48
  49/-- Neutral commutation predicate for adjacent syllables. Swapping preserves
  50ledger additivity and winding by construction; we additionally require the
  51start ticks to differ to avoid degenerate swaps. -/
  52@[simp] def neutralCommute (a b : Ribbon) : Bool := a.start ≠ b.start
  53
  54/-- A word is a list of ribbon syllables. -/
  55abbrev Word := List Ribbon
  56
  57/-- Deterministic ring pattern for a given tag: spread across ticks, alternate direction. -/
  58def ringSeq (tag : GaugeTag) (n : Nat) : Word :=
  59  (List.range n).map (fun k =>
  60    let t : Tick := ⟨k % 8, by have : (k % 8) < 8 := Nat.mod_lt _ (by decide); simpa using this⟩
  61    let d := k % 2 = 0
  62    { start := t, dir := d, bit := 1, tag := tag })
  63
  64/-- One left‑to‑right cancellation pass: drop the first adjacent cancelling pair if present. -/
  65def rewriteOnce : Word → Word :=
  66  fun w =>
  67    match w with
  68    | [] => []
  69    | a :: [] => [a]
  70    | a :: b :: rest =>
  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