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

Leaf actions retain the permutation written by classification.

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

Leaf actions consume the scratch permutation without resizing it.

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

Classifying a node may replace scratch entries but preserves its allocation.

theorem Hex.GraphIso.Nauty.scratchPolicy {n : Nat} (ctx : Ctx n) (inf tcLevel : Nat) : Generic.ReferencePolicy ctx inf tcLevel fun (st : Search n) => st.workperm.size

The off-path operations preserve the scratch allocation exactly.

theorem Hex.GraphIso.Nauty.node_workSize {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) : (node false ctx inf tcLevel fuel level numcells st).snd.workperm.size = st.workperm.size

An off-path node uses the allocated scratch array throughout the call.

theorem Hex.GraphIso.Nauty.sweep_workSize {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : Search n) (hpast : Generic.Past first tv1 cursor) : (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.workperm.size = st.workperm.size

Later siblings retain the same scratch allocation.

theorem Hex.GraphIso.Nauty.firstPath_workSize {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) : (node true ctx inf tcLevel fuel level numcells st).snd.workperm.size = st.workperm.size

The first descent does not use or resize the scratch allocation.

theorem Hex.GraphIso.Nauty.runState_workSize {n k : Nat} (G : Colored n k) : (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).snd.workperm.size = n

Every scratch scatter in a complete search run has its initial allocation size.