theorem Hex.GraphIso.Nauty.pruneReturn_short {n : Nat} {κ : Type} {level target : Nat} {st : SearchState n κ} (h : (pruneReturn level st).fst = Generic.Exit.unwind target true) : level ≠ st.noncheaplevel

The shared prune tail requests a short filter only after admitting its implicit pair at a level different from the saved boundary.

theorem Hex.GraphIso.Nauty.pruneReturn_bound {n : Nat} {κ : Type} {level target : Nat} {short : Bool} {st : SearchState n κ} (h : (pruneReturn level st).fst = Generic.Exit.unwind target short) : target ≤ st.noncheaplevel - 1

The implicit prune tail returns no deeper than the parent of its saved cheap boundary, including the signed-to-natural conversion.

theorem Hex.GraphIso.Nauty.leafExit_cheap_bound {n : Nat} {κ : Type} {level target : Nat} {short : Bool} {st : SearchState n κ} {leaf : Leaf} (ha : leaf = Generic.Leaf.bad ∨ ∃ (sr : Nat), leaf = Generic.Leaf.better sr) (h : (leafExit leaf level st).fst = Generic.Exit.unwind target short) : target ≤ st.noncheaplevel - 1

Both implicit-pair leaf actions use the same bounded return target.

theorem Hex.GraphIso.Nauty.leafExit_bound {n : Nat} {κ : Type} {level target : Nat} {short : Bool} {st : SearchState n κ} {leaf : Leaf} (hf : st.gcaFirst < level) (hc : st.gcaCanon < level) (hn : st.noncheaplevel ≤ level) (h : (leafExit leaf level st).fst = Generic.Exit.unwind target short) : target < level

With both saved ancestors below the node, every leaf return leaves that node. The implicit return also respects the saved cheap boundary.

theorem Hex.GraphIso.Nauty.leafExit_canon_target {n : Nat} {κ : Type} {level target : Nat} {st : SearchState n κ} (h : (leafExit Generic.Leaf.autoCanon level st).fst = Generic.Exit.unwind target true) : target = (leafExit Generic.Leaf.autoCanon level st).snd.gcaCanon

A short code-2 return targets the saved canonical ancestor.

theorem Hex.GraphIso.Nauty.leafExit_cheap_short {n : Nat} {κ : Type} {level target : Nat} {st : SearchState n κ} {leaf : Leaf} (ha : leaf = Generic.Leaf.bad ∨ ∃ (sr : Nat), leaf = Generic.Leaf.better sr) (h : (leafExit leaf level st).fst = Generic.Exit.unwind target true) : level ≠ st.noncheaplevel

A short return from a bad or better leaf satisfies the implicit-pair admission test used by that very leaf action.

theorem Hex.GraphIso.Nauty.leafExit_short_pair {n : Nat} {κ : Type} {st : SearchState n κ} (hcap : 0 < st.wsCap) {leaf : Leaf} {level target : Nat} (hexit : (leafExit leaf level st).fst = Generic.Exit.unwind target true) : leaf = Generic.Leaf.autoCanon ∧ (leafExit leaf level st).snd.autos.back? = some (fmperm st.workperm n) ∨ (leaf = Generic.Leaf.bad ∨ ∃ (sr : Nat), leaf = Generic.Leaf.better sr) ∧ (leafExit leaf level st).snd.autos.back? = some (fmptn st.lab st.ptn st.noncheaplevel n)

Each short-prune request exposes the pair admitted by the same leaf action. Only code 2 and the implicit prune tail can set this flag.

theorem Hex.GraphIso.Nauty.recover_autos {n : Nat} (inf level : Nat) (st : Search n) : (recover inf level st).autos = st.autos

Recovery retains the pruning workspace seen by the just-completed child.

theorem Hex.GraphIso.Nauty.recover_filters {n : Nat} (inf level : Nat) (cell : VSet n) (st : Search n) : have out := recover inf level st; longprune cell out.fixedpts out.autos = longprune cell st.fixedpts st.autos ∧ shortprune cell out = shortprune cell st

Both filters read the same workspace before and after parent recovery. This lets the restored partition justify the filter that ran just before it.