theorem Hex.GraphIso.Nauty.Generation.other_agreement {n : Nat} (ctx : Ctx n) (inf tcLevel floor fuel level numcells : Nat) (st : SearchSt n) : floor < level → floor ≤ st.eqlevFirst → floor ≤ (otherNode ctx inf tcLevel fuel level numcells st).snd.eqlevFirst

Off-path recursion cannot erase first-reference agreement strictly above its entry level. This follows the actual updates, without assuming that the comparison invariant records maximal agreement.

theorem Hex.GraphIso.Nauty.Generation.firstTail_agreement {n : Nat} (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (cursor : Option Nat) (tcell : VSet n) (index : Nat) (st : SearchSt n) : (∀ (v : Nat), cursor = some v → tv1 < v) → level ≤ st.eqlevFirst → level ≤ (firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor tcell index st).snd.snd.eqlevFirst

After the guiding vertex, every child is off-path and preserves the agreement at the receiving frame, including on early returns.

theorem Hex.GraphIso.Nauty.Generation.firstGuide_agreement {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)) (hs : level ≤ out.eqlevFirst) : level ≤ (firstChildLoop ctx inf tcLevel fuel (cfuel + 1) level numcells tc tv (some tv) tcell index st).snd.snd.eqlevFirst

Agreement installed by the guiding child survives the rest of its parent's sweep.