theorem
Hex.GraphIso.Nauty.Sparse.refineWith_frame
{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))
(h : NodeOk n level lab ptn active)
(hb : Scratch.Bounded n scratch)
(ancestor : Array Nat)
(base : Nat)
(hs : ancestor.size = n)
(hend : ancestor[n - 1]! ≤ base)
(hcoarse : ∀ (q : Nat), ancestor[q]! ≤ base → ptn[q]! ≤ level)
:
Refinement preserves every ancestor cell's vertex multiset, and retains the literal partition value at each boundary inherited from that ancestor.
theorem
Hex.GraphIso.Nauty.Sparse.refineWith_cellsReach
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(level : Nat)
(lab ptn : Array Nat)
(active : VSet n)
(numcells : Nat)
(scratch : Scratch)
(hp : lab.toList.Perm (List.range n))
(h : NodeOk n level lab ptn active)
(hb : Scratch.Bounded n scratch)
(hr : CellsReach G.toDense lab)
(hcoarse : ∀ (q : Nat), (initPtn n (n + 2) (Nauty.initialPartition G.toDense).snd)[q]! ≤ 1 → ptn[q]! ≤ level)
:
CellsReach G.toDense (refineWith (Graph.ofGraph G.graph) level lab ptn active numcells scratch).lab
Every sparse refinement preserves reachability within the original ordered colour cells. The dense coloured graph here interprets only the already proved ordered-partition bridge.
theorem
Hex.GraphIso.Nauty.Sparse.visit_cellsReach
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < 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)
(hr : CellsReach G.toDense s.lab)
(hcoarse : ∀ (q : Nat), (initPtn n (n + 2) (Nauty.initialPartition G.toDense).snd)[q]! ≤ 1 → s.ptn[q]! ≤ level)
:
CellsReach G.toDense (visit (Graph.ofGraph G.graph) level numcells s).snd.snd.lab
The actual production visit preserves the original ordered colour classes under the ancestor-boundary invariant.