structure Hex.GraphIso.Nauty.Sparse.Boundary (level : Nat) (before after : Array Nat) : Prop

Refinement only writes its current level into the partition array.

• size : after.size = before.size
• values (q : Nat) : after[q]! = before[q]! ∨ after[q]! = level

theorem Hex.GraphIso.Nauty.Sparse.Boundary.refl (level : Nat) (ptn : Array Nat) : Boundary level ptn ptn

theorem Hex.GraphIso.Nauty.Sparse.Boundary.trans {level : Nat} {a b c : Array Nat} (h : Boundary level a b) (h' : Boundary level b c) : Boundary level a c

theorem Hex.GraphIso.Nauty.Sparse.Boundary.set {level : Nat} {a b : Array Nat} (h : Boundary level a b) (i : Nat) : Boundary level a (b.setIfInBounds i level)

theorem Hex.GraphIso.Nauty.Sparse.Boundary.closed {level : Nat} {a b : Array Nat} (h : Boundary level a b) {q : Nat} (hq : a[q]! ≤ level) : b[q]! ≤ level

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_boundary {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) : Boundary level s.ptn (splitCounts level first distance s).ptn

The complete count splitter preserves old closed boundaries, including all indirect-sort, queue-replacement and distance-code branches.