neutralCommute

formal source

  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
  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