theorem Hex.GraphIso.Nauty.Sparse.SpecNode.refine_singleton {n : Nat} {G : SparseGraph n} {level numcells a : Nat} {lab ptn : Array Nat} {active : VSet n} (h : SpecNode G level lab ptn active numcells) (scratch : Scratch) (hs : Scratch.Bounded n scratch) (ha : IsCell ptn level a 1) : have out := Sparse.refineWith (Graph.ofGraph G) level lab ptn active numcells scratch; IsCell out.ptn level a 1 ∧ out.lab[a]! = lab[a]!

Cached native refinement retains both boundaries and the literal vertex of every incoming singleton.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.child_frame {n : Nat} {G : SparseGraph n} {level : Nat} {s : RefineSt n} (h : Ready G level s) {tc len o : Nat} (hc : IsCell s.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (scratch : Scratch) (hs : Scratch.Bounded n scratch) : have out := RefineSt.child (Graph.ofGraph G) level s tc s.lab[tc + o]! scratch; cellsPerm s.ptn level s.lab out.lab ∧ ∀ (q : Nat), s.ptn[q]! ≤ level → out.ptn[q]! = s.ptn[q]!

An actual cached child preserves its parent's ordered cell contents and every boundary already closed at that parent.

theorem Hex.GraphIso.Nauty.Sparse.DescPath.frame {n : Nat} {G : SparseGraph n} {base last : Nat} {root leaf : RefineSt n} {path : List (Nat × Nat)} (h : DescPath G base root path last leaf) (hr : RefineSt.Ready G base root) : cellsPerm root.ptn base root.lab leaf.lab ∧ ∀ (q : Nat), root.ptn[q]! ≤ base → leaf.ptn[q]! = root.ptn[q]!

Every literal native descent retains its frozen ancestor's cell contents and closed boundaries, independently of scratch contents.