pith. machine review for the scientific record. sign in
def definition def or abbrev

ringSeq

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  58def ringSeq (tag : GaugeTag) (n : Nat) : Word :=

proof body

Definition body.

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

depends on (10)

Lean names referenced from this declaration's body.