theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_capacity {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (chooseTarget first g tcLevel level numcells st).snd.snd.snd.wsCap = st.wsCap

Native target selection retains the pruning workspace capacity.

theorem Hex.GraphIso.Nauty.Sparse.classify_capacity {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : (classify g level numcells st).snd.wsCap = st.wsCap

Both native automorphism scatters retain the pruning workspace capacity.

theorem Hex.GraphIso.Nauty.Sparse.capacityPolicy {n : Nat} (g : Graph n) (inf tcLevel size : Nat) : Generic.Preserve g inf tcLevel fun (st : State n) => st.wsCap = size

Every executed policy operation preserves the pair capacity, on the first descent as well as later siblings and nonlocal returns.

theorem Hex.GraphIso.Nauty.Sparse.node_capacity {n : Nat} (first : Bool) (g : Graph n) (inf tcLevel fuel level numcells : Nat) (st : State n) : (Generic.node first g inf tcLevel fuel level numcells st).snd.wsCap = st.wsCap

theorem Hex.GraphIso.Nauty.Sparse.sweep_capacity {n : Nat} (first : Bool) (g : Graph n) (inf tcLevel fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) : (Generic.sweep first g inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.wsCap = st.wsCap

theorem Hex.GraphIso.Nauty.Sparse.runState_capacity {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : (runState g lab ends).snd.wsCap = 500

The initialized native search retains its pinned 500-pair capacity, including order zero, independently of label or graph validity.

theorem Hex.GraphIso.Nauty.Sparse.run_capacity {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : (run g lab ends).wsCap = 500