theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_ready {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : NodeInv G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) : have r := visit (Graph.ofGraph G.graph) level numcells st; Ready G level r.fst r.snd.snd

A production visit establishes the equitable parent invariant and a valid cache, retaining exact counts and original colour-cell boundaries.

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_frame {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : NodeInv G level numcells st) (hl : 1 ≤ level) {out : State n} (hx : FrameOut G level level (visit (Graph.ofGraph G.graph) level numcells st).snd.snd out) : FrameOut G (level - 1) level st out

Compose an executed refinement with the rest of its node. New cuts are below the receiving ancestor, while labels and stored references stay within the caller's cells. This follows the sparse operation's actual write sites.