structure Hex.GraphIso.Nauty.Sparse.RefineSt.Valid {n : Nat} (level : Nat) (s : RefineSt n) : Prop

The indexed working state has a permutation labelling, a closed bounded partition, exact cell indices, allocated scratch, and an exact active queue.

• lab : s.lab.toList.Perm (List.range n)
• size : s.ptn.size = n
• closed : s.ptn[n - 1]! ≤ level
• index : Index.Valid n s.lab s.ptn level s.cellstart s.cellend
• scratch : Scratch.Bounded n s.toScratch
• queue : CellQueue s.ptn level s.active s.queue

structure Hex.GraphIso.Nauty.Sparse.RefineSt.Step {n : Nat} (level : Nat) (s t : RefineSt n) : Prop

A refinement pass subdivides the original cells, retaining their vertex multisets and charging the cell counter once for each new boundary.

• cuts : Cuts level n s.ptn t.ptn s.numcells t.numcells n
• cells : cellsPerm s.ptn level t.lab s.lab

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Step.refl {n : Nat} (level : Nat) (s : RefineSt n) : Step level s s

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Step.trans {n level : Nat} {s t u : RefineSt n} (h : Step level s t) (k : Step level t u) (hs : Valid level s) (ht : Valid level t) (hu : Valid level u) : Step level s u

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.hash {n level : Nat} {s : RefineSt n} (h : Valid level s) (v : Nat) : Valid level (s.hash v)

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.remove {n level : Nat} {s : RefineSt n} (h : Valid level s) {pos : Nat} (hp : pos < s.queue.size) : Valid level { lab := s.lab, ptn := s.ptn, active := s.active.erase s.queue[pos]!, queue := (s.queue.setIfInBounds pos s.queue[s.queue.size - 1]!).pop, cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.cell {n level : Nat} {s : RefineSt n} (h : Valid level s) {first : Nat} (hf : first < n) (ha : first = 0 ∨ s.ptn[first - 1]! ≤ level) : IsCell s.ptn level first (s.cellend[first]! + 1 - first) ∧ first ≤ s.cellend[first]! ∧ s.cellend[first]! < n

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.queue_cell {n level : Nat} {s : RefineSt n} (h : Valid level s) {pos : Nat} (hp : pos < s.queue.size) : s.queue[pos]! < n ∧ IsCell s.ptn level s.queue[pos]! (s.cellend[s.queue[pos]!]! + 1 - s.queue[pos]!) ∧ s.queue[pos]! ≤ s.cellend[s.queue[pos]!]! ∧ s.cellend[s.queue[pos]!]! < n

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.counts {n level : Nat} {s : RefineSt n} (h : Valid level s) (first : Nat) (distance : Bool) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) : Valid level (splitCounts level first distance s) ∧ Step level s (splitCounts level first distance s)

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.singleton {n level : Nat} {s : RefineSt n} (h : Valid level s) (G : SparseGraph n) (split : Nat) (hb : split < n) : Valid level (splitSingleton (Graph.ofGraph G) level split s) ∧ Step level s (splitSingleton (Graph.ofGraph G) level split s)

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.nontrivial {n level : Nat} {s : RefineSt n} (h : Valid level s) (G : SparseGraph n) (split len : Nat) (hc : IsCell s.ptn level split len) (hb : split + len ≤ n) : Valid level (splitNontrivial (Graph.ofGraph G) level split s) ∧ Step level s (splitNontrivial (Graph.ofGraph G) level split s)