inductive Hex.GraphIso.Nauty.RefReturn {n : Nat} {κ : Type} (ctx : Ctx n) (target : Nat) (out : SearchState n κ) : Prop

A returned generator retains its reference endpoint or its strictly smaller coset image. Cleanup does not erase this evidence.

• first {n : Nat} {κ : Type} {ctx : Ctx n} {target : Nat} {out : SearchState n κ} (returned : target = out.gcaFirst) (carrier : LabelCarrier ctx out.firstlab out.lab out.genTrace) : RefReturn ctx target out
• canon {n : Nat} {κ : Type} {ctx : Ctx n} {target : Nat} {out : SearchState n κ} (returned : target = out.gcaCanon) (carrier : LabelCarrier ctx out.canonlab out.lab out.genTrace) : RefReturn ctx target out
• orbit {n : Nat} {κ : Type} {ctx : Ctx n} {target : Nat} {out : SearchState n κ} (returned : target = out.gcaFirst) (smaller : out.orbits[out.cosetindex]! < out.cosetindex) : RefReturn ctx target out

theorem Hex.GraphIso.Nauty.pruneReturn_boundary {n : Nat} {κ : Type} {level target : Nat} {st : SearchState n κ} {short : Bool} (he : (pruneReturn level st).fst = Generic.Exit.unwind target short) : st.noncheaplevel ≤ target + 1 ∨ st.allsamelevel ≤ target + 1

A comparison prune can only return below one of its two saved subtree boundaries. This statement has no generator premise.

theorem Hex.GraphIso.Nauty.classify_first_map {n : Nat} {ctx : Ctx n} {level numcells : Nat} {before out : Search n} (hc : classify ctx level numcells before = (Generic.Leaf.autoFirst, out)) (hw : out.workperm.size = n) (hf : out.firstlab.size = n) (hp : out.firstlab.toList.Perm (List.range n)) (i : Nat) : i < n → out.workperm[out.firstlab[i]!]! = out.lab[i]!

A first-reference classification supplies the scatter's complete pointwise action using the returned scratch and reference sizes.

theorem Hex.GraphIso.Nauty.leaf_refReturn {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells target : Nat} {before : Search n} {short : Bool} (hn0 : 0 < n) (ha : (classify ctx level numcells before).fst = Generic.Leaf.autoFirst ∨ (classify ctx level numcells before).fst = Generic.Leaf.autoCanon) (he : (leafExit (classify ctx level numcells before).fst level (classify ctx level numcells before).snd).fst = Generic.Exit.unwind target short) (hi : RunInv G ctx (leafExit (classify ctx level numcells before).fst level (classify ctx level numcells before).snd).snd) : RefReturn ctx target (leafExit (classify ctx level numcells before).fst level (classify ctx level numcells before).snd).snd

Every automorphism verdict carries evidence after its leaf action, including canonical returns that do not merge any orbit.

theorem Hex.GraphIso.Nauty.leaf_boundary {n : Nat} {κ : Type} {leaf : Leaf} {level target : Nat} {st : SearchState n κ} {short : Bool} (hf : leaf ≠ Generic.Leaf.autoFirst) (hc : leaf ≠ Generic.Leaf.autoCanon) (he : (leafExit leaf level st).fst = Generic.Exit.unwind target short) : (leafExit leaf level st).snd.noncheaplevel ≤ target + 1 ∨ (leafExit leaf level st).snd.allsamelevel ≤ target + 1

Every non-generator leaf exit is bounded by a saved subtree boundary, including installation of a better canonical leaf.

theorem Hex.GraphIso.Nauty.RefReturn.fixed {n : Nat} {κ : Type} {ctx : Ctx n} {target : Nat} {st : SearchState n κ} (h : RefReturn ctx target st) (fixed : VSet n) : RefReturn ctx target { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := fixed, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace, workperm := st.workperm }

Fixed-point cleanup preserves the emitted reference carrier.

theorem Hex.GraphIso.Nauty.EarlyReturn.reference {n k : Nat} {G : Colored n k} {ctx : Ctx n} {target bound : Nat} {short : Bool} {out : Search n} (h : EarlyReturn ctx target short out) (hn0 : 0 < n) (hi : RunInv G ctx out) (ht : target < bound) (hn : bound < out.noncheaplevel) (ha : bound < out.allsamelevel) : RefReturn ctx target out

An actual unconsumed return above both subtree boundaries carries the emitted automorphism evidence through every intermediate cleanup.

theorem Hex.GraphIso.Nauty.leaf_short_first {n : Nat} {κ : Type} {leaf : Leaf} {level target : Nat} {st : SearchState n κ} (hpos : 0 < target) (he : (leafExit leaf level st).fst = Generic.Exit.unwind target true) : target ≠ (leafExit leaf level st).snd.gcaFirst

A short-prune request never targets the emitting first ancestor.

theorem Hex.GraphIso.Nauty.node_short_first {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells target : Nat} {st : Search n} (hpos : 0 < target) (he : (node false ctx inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target true) : target ≠ st.gcaFirst

An off-path node cannot request short pruning at its first ancestor. Only an enclosing first-child update could change that ancestor.