theorem Hex.GraphIso.Nauty.Sparse.visit_shape {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) (hs : st.ptn.size = n) (hend : st.ptn[n - 1]! ≤ level) (h : NodeShape n level st.ptn) : NodeShape n level (visit g level numcells st).snd.snd.ptn

The full native refinement preserves every cheap-guard shape. Only its proved boundary writes matter; cache state and splitter order do not.

theorem Hex.GraphIso.Nauty.Sparse.child_shape {n : Nat} (first : Bool) (level tc tv : Nat) (st : State n) (hs : st.ptn.size = n) (hend : st.ptn[n - 1]! ≤ level) (h : NodeShape n level st.ptn) : NodeShape n (level + 1) (Generic.Policy.child first level tc tv st).ptn

The actual child transition preserves the cheap shape by adding its singleton boundary. Refinement of that child preserves it again.

theorem Hex.GraphIso.Nauty.Sparse.Ready.child_small {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hshape : NodeShape n level st.ptn) (first : Bool) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) : have child := Generic.Policy.child first level tc tv st; have r := visit (Graph.ofGraph G.graph) (level + 1) (numcells + 1) child; Ready G (level + 1) r.fst r.snd.snd ∧ NodeShape n (level + 1) r.snd.snd.ptn

Every selected native child below a cheap-shaped equitable parent returns an equitable partition of the same shape after its actual visit.