theorem Hex.GraphIso.Nauty.workspace_push {n : Nat} {st : Search n} (h : WorkspaceOk st) (pair : VSet n × VSet n) : WorkspaceOk (pushAuto st pair)

Search insertion obeys the bounded workspace invariant.

theorem Hex.GraphIso.Nauty.workspace_admit {n : Nat} {st : Search n} (h : WorkspaceOk st) : WorkspaceOk (admit st)

Explicit generator admission keeps the capacity and bounded pair array.

theorem Hex.GraphIso.Nauty.workspace_prune {n : Nat} {st : Search n} (h : WorkspaceOk st) (level : Nat) : WorkspaceOk (pruneReturn level st).snd

Inserting the frozen implicit pair preserves workspace bounds.

theorem Hex.GraphIso.Nauty.workspace_leaf {n : Nat} {st : Search n} (h : WorkspaceOk st) (leaf : Leaf) (level : Nat) : WorkspaceOk (leafExit leaf level st).snd

Every leaf action preserves the bounded workspace, independently of the automorphism and subtree proofs that justify its admitted pair.

theorem Hex.GraphIso.Nauty.leafExit_capacity {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.wsCap = st.wsCap

Leaf emission retains the capacity used by its pair insertion.

theorem Hex.GraphIso.Nauty.classify_capacity {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : (classify ctx level numcells st).snd.wsCap = st.wsCap

Classification changes neither the workspace capacity nor its pair array.