theorem Hex.GraphIso.Nauty.matching_target {n : Nat} {ctx : Ctx n} {tcLevel level numcells tc : Nat} {st : Search n} {rs : RefineSt n} {targets : List Nat} {key : Key n} (hit : IterOk ctx level rs) (heqt : Equitable ctx level rs.lab rs.ptn) (hlab : st.lab = rs.lab) (hptn : st.ptn = rs.ptn) (hn : numcells < n) (hm : Generation.Matches ctx level st (tc :: targets) key) (hp : Generation.HasLeaf ctx tcLevel level rs (tc :: targets) key) (heq : st.eqlevFirst = level) : have t := specMaketargetcell ctx rs.lab rs.ptn level tcLevel; chooseTarget false ctx tcLevel level numcells st = (Int.ofNat t.fst, t.snd.fst, t.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, 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 + t.snd.snd, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace, workperm := st.workperm })

A matching occurrence prevents a first-target hint from changing the selected cell or demoting the first-reference comparison.

theorem Hex.GraphIso.Nauty.descent_reference {n : Nat} {ctx : Ctx n} (inf tcLevel : Nat) (hgsz : ctx.g.size = n) (P : Nat → RefineSt n → List Nat → Key n → Prop) (hvalid : ∀ {level : Nat} {rs : RefineSt n} {targets : List Nat} {key : Key n}, P level rs targets key → IterOk ctx level rs ∧ Equitable ctx level rs.lab rs.ptn ∧ bcount rs.ptn level n = rs.numcells) (hchildren : ∀ {level : Nat} {rs : RefineSt n} {tc e o : Nat} {targets : List Nat} {key : Key n}, P level rs (tc :: targets) { codes := rs.longcode :: key.codes, rows := key.rows } → level < n → (tc, e) ∈ cells rs.ptn level n → tc < e → tc = specTargetcell ctx rs.lab rs.ptn level tcLevel → o ≤ e - tc → Generation.HasLeaf ctx tcLevel (level + 1) (childSt ctx level rs tc rs.lab[tc + o]!) targets key → ∀ (o' : Nat), o' ≤ e - tc → P (level + 1) (childSt ctx level rs tc rs.lab[tc + o']!) targets key ∧ Generation.HasLeaf ctx tcLevel (level + 1) (childSt ctx level rs tc rs.lab[tc + o']!) targets key) (fuel level numcells : Nat) (st : Search n) (targets : List Nat) (key : Key n) : P level (SearchState.refined ctx level numcells st) targets key → st.workperm.size = n → st.firstlab.size = n → st.firstlab.toList.Perm (List.range n) → Generation.Matches ctx level st targets key → Generation.HasLeaf ctx tcLevel level (SearchState.refined ctx level numcells st) targets key → st.eqlevFirst = level - 1 → st.gcaFirst < level → n < level + fuel → have out := node false ctx inf tcLevel fuel level numcells st; out.fst = Generic.Exit.unwind st.gcaFirst false ∧ LabelCarrier ctx st.firstlab out.snd.lab out.snd.genTrace

A reference that continues through every target child makes the actual first descent emit a carrier. The same recursion handles small cells and uniform subtrees.

theorem Hex.GraphIso.Nauty.cheap_reference {n : Nat} {ctx : Ctx n} (inf tcLevel : Nat) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (fuel level numcells : Nat) (st : Search n) (targets : List Nat) (key : Key n) : SubtreeOk ctx level (SearchState.refined ctx level numcells st) → st.workperm.size = n → st.firstlab.size = n → st.firstlab.toList.Perm (List.range n) → Generation.Matches ctx level st targets key → Generation.HasLeaf ctx tcLevel level (SearchState.refined ctx level numcells st) targets key → st.eqlevFirst = level - 1 → st.gcaFirst < level → n < level + fuel → have out := node false ctx inf tcLevel fuel level numcells st; out.fst = Generic.Exit.unwind st.gcaFirst false ∧ LabelCarrier ctx st.firstlab out.snd.lab out.snd.genTrace

A matching small-cell node follows its actual first child to an emitted automorphism, without assuming a generated carrier.

theorem Hex.GraphIso.Nauty.uniform_reference {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells : Nat} {st : Search n} {targets : List Nat} {key : Key n} (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hT : Generation.TreeOk ctx level (SearchState.refined ctx level numcells st)) (hU : Generation.Uniform ctx tcLevel level (SearchState.refined ctx level numcells st) targets key) (hw : st.workperm.size = n) (hf : st.firstlab.size = n) (hfp : st.firstlab.toList.Perm (List.range n)) (hm : Generation.Matches ctx level st targets key) (heq : st.eqlevFirst = level - 1) (hg : st.gcaFirst < level) (hbudget : n < level + fuel) : have out := node false ctx inf tcLevel fuel level numcells st; out.fst = Generic.Exit.unwind st.gcaFirst false ∧ LabelCarrier ctx st.firstlab out.snd.lab out.snd.genTrace

Uniformity of a valid matching subtree forces a recorded generator on the actual first descent. Validity supplies leaf existence.