theorem Hex.GraphIso.Nauty.compareCodes_frame {n : Nat} {κ : Type} (level code : Nat) (st : SearchState n κ) : have out := compareCodes level code st; out.lab = st.lab ∧ out.ptn = st.ptn ∧ out.firstlab = st.firstlab ∧ out.canonlab = st.canonlab

Code comparison changes no partition or leaf-reference array.

theorem Hex.GraphIso.Nauty.chooseTarget_frame {n : Nat} (first : Bool) (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : have out := (chooseTarget first ctx tcLevel level numcells st).snd.snd.snd; out.lab = st.lab ∧ out.ptn = st.ptn ∧ out.firstlab = st.firstlab ∧ out.canonlab = st.canonlab

Target selection changes no partition or leaf-reference array.

theorem Hex.GraphIso.Nauty.leafExit_done {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).fst = Generic.Exit.done ↔ leaf = Generic.Leaf.internal

Only an internal classification continues the current node.

theorem Hex.GraphIso.Nauty.pruneReturn_noFuel {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : (pruneReturn level st).fst ≠ Generic.Exit.fuel

Pruning returns an ancestor level without consuming recursion fuel.

theorem Hex.GraphIso.Nauty.leafExit_noFuel {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).fst ≠ Generic.Exit.fuel

Leaf actions return control without consuming recursion fuel.

theorem Hex.GraphIso.Nauty.classify_internal {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : (classify ctx level numcells st).fst = Generic.Leaf.internal ↔ ¬(st.eqlevFirst ≠ level ∧ st.compCanon < 0) ∧ numcells ≠ n

The internal classification is exactly a non-discrete node that has not failed both first-path and canonical comparison.

theorem Hex.GraphIso.Nauty.classify_frame {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : have out := (classify ctx level numcells st).snd; out.lab = st.lab ∧ out.ptn = st.ptn ∧ out.firstlab = st.firstlab ∧ out.canonlab = st.canonlab

Classification preserves the partition and both saved labellings.

theorem Hex.GraphIso.Nauty.admit_frame {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).lab = st.lab ∧ (admit st).ptn = st.ptn ∧ (admit st).firstlab = st.firstlab ∧ (admit st).canonlab = st.canonlab

Admitting a generator does not change the partition or leaf references.

theorem Hex.GraphIso.Nauty.pruneReturn_frame {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : have out := (pruneReturn level st).snd; out.lab = st.lab ∧ out.ptn = st.ptn ∧ out.firstlab = st.firstlab ∧ out.canonlab = st.canonlab

A pruning return changes neither the partition nor the leaf references.

theorem Hex.GraphIso.Nauty.leafExit_frame {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : have out := (leafExit leaf level st).snd; out.lab = st.lab ∧ out.ptn = st.ptn ∧ out.firstlab = st.firstlab ∧ (out.canonlab = st.canonlab ∨ out.canonlab = st.lab)

Processing a leaf preserves the current partition and first leaf; the canonical labelling is retained or replaced by the current labelling.

theorem Hex.GraphIso.Nauty.frame_ok {n k : Nat} {G : Colored n k} {level numcells : Nat} {st out : Search n} (hok : SearchOk G level numcells st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) (hc : out.canonlab = st.canonlab ∨ out.canonlab = st.lab) : SearchOk G level numcells out

Changing bookkeeping and optionally installing the current labelling preserves the partition invariant.

theorem Hex.GraphIso.Nauty.frame_out {n k : Nat} {G : Colored n k} {B level numcells : Nat} {st out : Search n} (hok : SearchOk G level numcells st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) (hf : out.firstlab = st.firstlab ∨ out.firstlab = st.lab) (hc : out.canonlab = st.canonlab ∨ out.canonlab = st.lab) : SearchOut G B level st out

A local operation with unchanged partition and only current-leaf installations satisfies the call's frame effect.

theorem Hex.GraphIso.Nauty.leaf_ok {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (hok : SearchOk G level numcells st) : have verdict := classify ctx level numcells st; SearchOk G level numcells (leafExit verdict.fst level verdict.snd).snd

Classification and the resulting leaf action preserve the partition invariant, independently of whether the classification is sound.

theorem Hex.GraphIso.Nauty.leaf_out {n k : Nat} {G : Colored n k} {ctx : Ctx n} {B level numcells : Nat} {st : Search n} (hok : SearchOk G level numcells st) : have verdict := classify ctx level numcells st; SearchOut G B level st (leafExit verdict.fst level verdict.snd).snd

The combined leaf operations have only the permitted frame effect.