theorem Hex.GraphIso.Nauty.Generation.prune_floor {level noncheaplevel allsamelevel : Nat} {eqlevCanon : Int} (hcheap : level < noncheaplevel) (hsame : level < allsamelevel) : Int.ofNat level ≤ pruneReturn noncheaplevel allsamelevel eqlevCanon

A non-generator prune cannot cross an ancestor that lies strictly above both saved subtree boundaries, regardless of the canonical comparison.

theorem Hex.GraphIso.Nauty.Generation.prune_floor_canon {level noncheaplevel allsamelevel : Nat} {eqlevCanon : Int} (hcheap : level < noncheaplevel) (hcanon : Int.ofNat level ≤ eqlevCanon) : Int.ofNat level ≤ pruneReturn noncheaplevel allsamelevel eqlevCanon

Agreement with the canonical prefix also prevents a non-generator prune from crossing this level, independently of the all-same boundary.

theorem Hex.GraphIso.Nauty.Generation.prune_early {level noncheaplevel allsamelevel : Nat} {eqlevCanon : Int} (h : pruneReturn noncheaplevel allsamelevel eqlevCanon < Int.ofNat level) : noncheaplevel ≤ level ∨ allsamelevel ≤ level

A non-generator return crossing an ancestor must use one of the two saved subtree boundaries. A comparison-code argument alone is insufficient.

theorem Hex.GraphIso.Nauty.Generation.finish_floor {n level size index : Nat} {st : SearchSt n} (h : level ≤ st.allsamelevel) : level ≤ (firstFinish level size index st).allsamelevel

The final all-same adjustment never moves the boundary above the first-path frame being completed.

theorem Hex.GraphIso.Nauty.Generation.finish_drop {n level size index : Nat} {st : SearchSt n} (hbefore : level < st.allsamelevel) (hafter : (firstFinish level size index st).allsamelevel ≤ level) : size = index ∧ st.allsamelevel = level + 1

Lowering the all-same boundary to the completed frame requires both a uniform child boundary and a counter equal to the original cell size.