structure Hex.GraphIso.Nauty.Generation.FirstFields {n : Nat} (st out : SearchSt n) : Prop

Equality of the stored first reference, including its target hints and all-same boundary.

• codes : out.firstcode = st.firstcode
• targets : out.firsttc = st.firsttc
• lab : out.firstlab = st.firstlab
• same : out.allsamelevel = st.allsamelevel

theorem Hex.GraphIso.Nauty.Generation.FirstFields.refl {n : Nat} (st : SearchSt n) : FirstFields st st

theorem Hex.GraphIso.Nauty.Generation.FirstFields.trans {n : Nat} {a b c : SearchSt n} (h : FirstFields a b) (h' : FirstFields b c) : FirstFields a c

theorem Hex.GraphIso.Nauty.Generation.FirstFields.matching {n : Nat} {a b : SearchSt n} {ctx : Ctx n} {level : Nat} {targets : List Nat} {key : Key n} (h : FirstFields a b) (hm : Matches ctx level a targets key) : Matches ctx level b targets key

theorem Hex.GraphIso.Nauty.Generation.FirstFields.process {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : FirstFields st (processnode ctx level numcells st).snd

theorem Hex.GraphIso.Nauty.Generation.FirstFields.recover {n : Nat} (inf level : Nat) (st : SearchSt n) : FirstFields st (Nauty.recover n inf level st)

theorem Hex.GraphIso.Nauty.Generation.other_fields {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) : FirstFields st (otherNode ctx inf tcLevel fuel level numcells st).snd

Off-path recursion preserves the first reference's codes, hints, labelling, and all-same boundary, independently of all pruning and return choices.

theorem Hex.GraphIso.Nauty.Generation.other_boundary {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells : Nat} {st : SearchSt n} (hclear : st.needshortprune = false) (hboundary : st.gcaFirst < st.allsamelevel) : (otherNode ctx inf tcLevel fuel level numcells st).snd.gcaFirst < (otherNode ctx inf tcLevel fuel level numcells st).snd.allsamelevel

The saved all-same boundary remains strictly deeper than the first-path guide throughout an off-path subtree.

theorem Hex.GraphIso.Nauty.Generation.firstTail_fields {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) → FirstFields st (firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor tcell index st).snd.snd

Once the guiding vertex has been visited, a first-path sibling sweep preserves the complete stored first reference. All later recursive calls are off-path, including after target-set filters.

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

After the guiding recursive call, every remaining first-path sibling retains the exact reference that call installed. This includes early unwinds and the short-prune/recovery path.