theorem Hex.GraphIso.Nauty.Generation.process_retains {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} {γ : Array Nat} (hγ : γ ∈ st.genTrace) : γ ∈ (processnode ctx level numcells st).snd.genTrace

Recording an automorphism never discards earlier trace entries.

theorem Hex.GraphIso.Nauty.Generation.other_retains {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) {γ : Array Nat} : γ ∈ st.genTrace → γ ∈ (otherNode ctx inf tcLevel fuel level numcells st).snd.genTrace

Off-path recursion keeps all previously recorded generators.

theorem Hex.GraphIso.Nauty.Generation.first_retains {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) {γ : Array Nat} : γ ∈ st.genTrace → γ ∈ (firstPathNode ctx inf tcLevel fuel level numcells st).snd.genTrace

First-path recursion keeps all previously recorded generators, even when a bounded pruning-workspace slot is overwritten.

theorem Hex.GraphIso.Nauty.Generation.firstGuide_retains {n : Nat} {ctx : Ctx n} {inf tcLevel fuel cfuel level numcells tc tv index : Nat} {tcell : VSet n} {st out : SearchSt n} {r : Int} (hrep : (st.orbits[tv]! == tv) = true) (hcall : firstPathNode ctx inf tcLevel fuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 := tv, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } = (r, out)) {γ : Array Nat} (hγ : γ ∈ out.genTrace) : γ ∈ (firstChildLoop ctx inf tcLevel fuel (cfuel + 1) level numcells tc tv (some tv) tcell index st).snd.snd.genTrace

Every generator discovered by the guiding child remains in the completed sibling sweep, including when that child returns early.