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

Native target selection retains the permutation workspace allocation.

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

Both native automorphism scatters reuse the existing allocation.

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

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

theorem Hex.GraphIso.Nauty.Sparse.node_workSize {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.workperm.size = st.workperm.size

theorem Hex.GraphIso.Nauty.Sparse.sweep_workSize {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.workperm.size = st.workperm.size

theorem Hex.GraphIso.Nauty.Sparse.runState_workSize {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : (runState g lab ends).snd.workperm.size = n

The actual root has a workspace slot for every vertex, including the empty graph. No label or graph-validity hypothesis is needed for allocation.

theorem Hex.GraphIso.Nauty.Sparse.run_workSize {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : (run g lab ends).workperm.size = n