theorem
Hex.GraphIso.Nauty.Sparse.refineWith_count
{n : Nat}
(G : SparseGraph n)
(level : Nat)
(lab ptn : Array Nat)
(active : VSet n)
(numcells : Nat)
(scratch : Scratch)
(hp : lab.toList.Perm (List.range n))
(hs : ptn.size = n)
(hend : ptn[n - 1]! ≤ level)
(ha : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level)
(hb : Scratch.Bounded n scratch)
(hc : numcells = bcount ptn level n)
:
have t := refineWith (Graph.ofGraph G) level lab ptn active numcells scratch;
t.numcells = bcount t.ptn level n
Exact incoming accounting remains exact after the complete refinement.
theorem
Hex.GraphIso.Nauty.Sparse.visit_valid
{n : Nat}
(G : SparseGraph n)
(level numcells : Nat)
(s : State n)
(hp : s.lab.toList.Perm (List.range n))
(hs : s.ptn.size = n)
(hend : s.ptn[n - 1]! ≤ level)
(ha : ∀ (v : Nat), s.active.mem v = true → v = 0 ∨ s.ptn[v - 1]! ≤ level)
(hb : Scratch.Bounded n s.canong.scratch)
:
have t := (visit (Graph.ofGraph G) level numcells s).snd.snd;
Scratch.Valid n t.lab t.ptn level t.canong.scratch
The production visit returns a cache valid for its actual refined node.
theorem
Hex.GraphIso.Nauty.Sparse.visit_nodeOk
{n : Nat}
(G : SparseGraph n)
(level numcells : Nat)
(s : State n)
(hp : s.lab.toList.Perm (List.range n))
(h : NodeOk n level s.lab s.ptn s.active)
(hb : Scratch.Bounded n s.canong.scratch)
:
All partition-state facts required by search survive the sparse visit, including the sentinel values used by individualization and recovery.