theorem Hex.GraphIso.Nauty.chooseFirst_fields {n : Nat} (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : have r := chooseTarget true ctx tcLevel level numcells st; r.snd.snd.snd = { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc.set! level r.fst, 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 := r.snd.snd.snd.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 }

Selecting a first-path target only writes its target slot and counter.

theorem Hex.GraphIso.Nauty.prepareFirst_orbits {n : Nat} (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd.orbits = st.orbits

A first-path preparation preserves the orbit array.

theorem Hex.GraphIso.Nauty.chooseFirst_nonempty {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (hnc : numcells < n) : (chooseTarget true ctx tcLevel level numcells st).snd.fst ≠ VSet.empty

A nontrivial first-path target contains a vertex.

theorem Hex.GraphIso.Nauty.prepareFirst_ok {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) : have r := Generic.prepareFirst ctx tcLevel level numcells st; SearchOk G level r.fst r.snd.snd.snd.snd ∧ Generic.Target (fun (st : Search n) => st) level r.snd.fst.toNat r.snd.snd.fst r.snd.snd.snd.snd

Refining and selecting a first-path node preserves partition validity.

theorem Hex.GraphIso.Nauty.firstPath_exists {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells : Nat} {st : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (horbit : ∀ (v : Nat), v < n → st.orbits[v]! = v) (hfuel : n + 1 ≤ level + fuel) : ∃ (last : Nat), ∃ (leaf : Search n), Generic.FirstPath ctx tcLevel fuel level numcells st last leaf

Every valid first-path state with identity orbits reaches a first leaf within the same depth bound used by the executable search.

theorem Hex.GraphIso.Nauty.firstPath_reference {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) : SearchState.reference (node true ctx inf tcLevel fuel level numcells st).snd = (firstterminal last leaf).reference

A valid first-path search call returns the reference installed at its actual first leaf; subsequent sibling search cannot replace it.

theorem Hex.GraphIso.Nauty.initial_path {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : ∃ (last : Nat), ∃ (leaf : Search n), Generic.FirstPath { g := rowsOf G } 100 (n + 2) 1 (initialPartition G).snd.length (initial n (initialPartition G).fst (initialPartition G).snd) last leaf

The nonempty initial state has a successful first descent at the root bound.