structure Hex.GraphIso.Nauty.Sparse.Cuts (level n : Nat) (before ptn : Array Nat) (old count upto : Nat) : Prop

A sequence of increasing partition cuts charges the cell counter exactly once per new boundary, leaving the unprocessed suffix untouched.

• size : ptn.size = before.size
• count : bcount ptn level n + old = bcount before level n + count
• tail (q : Nat) : upto ≤ q → ptn[q]! = before[q]!
• closed (q : Nat) : before[q]! ≤ level → ptn[q]! = before[q]!

theorem Hex.GraphIso.Nauty.Sparse.Cuts.refl (level n : Nat) (ptn : Array Nat) (count upto : Nat) : Cuts level n ptn ptn count count upto

theorem Hex.GraphIso.Nauty.Sparse.Cuts.move {level n old count upto next : Nat} {before ptn : Array Nat} (h : Cuts level n before ptn old count upto) (hu : upto ≤ next) : Cuts level n before ptn old count next

theorem Hex.GraphIso.Nauty.Sparse.Cuts.cut {level n old count upto q : Nat} {before ptn : Array Nat} (h : Cuts level n before ptn old count upto) (hq : upto ≤ q) (hn : q < n) (hs : q < before.size) (ho : level < before[q]!) : Cuts level n before (ptn.setIfInBounds q level) old (count + 1) (q + 1)

theorem Hex.GraphIso.Nauty.Sparse.Cuts.initial {level n upto q : Nat} (ptn : Array Nat) (count : Nat) (hq : q < upto) (hn : q < n) (hs : q < ptn.size) (ho : level < ptn[q]!) : Cuts level n ptn (ptn.setIfInBounds q level) count (count + 1) upto

theorem Hex.GraphIso.Nauty.Sparse.Cuts.initial_count {level n q : Nat} (ptn : Array Nat) (count : Nat) (hn : q < n) (hs : q < ptn.size) (ho : level < ptn[q]!) : bcount (ptn.setIfInBounds q level) level n + count = bcount ptn level n + (count + 1)

theorem Hex.GraphIso.Nauty.Sparse.Cuts.trans {level n old count upto : Nat} {before ptn middle : Array Nat} {middleCount : Nat} (h : Cuts level n before middle old middleCount upto) (h' : Cuts level n middle ptn middleCount count upto) : Cuts level n before ptn old count upto

Successive passes compose their exact counter changes and retain every inherited closed value.

theorem Hex.GraphIso.Nauty.Sparse.Cuts.insert {level n old count q : Nat} {before ptn : Array Nat} (h : Cuts level n before ptn old count n) (hn : q < n) (hs : q < ptn.size) (ho : level < ptn[q]!) : Cuts level n before (ptn.setIfInBounds q level) old (count + 1) n

Closing one open position extends an already completed pass.