theorem Hex.GraphIso.Nauty.Generation.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 → 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 ∧ HasLeaf ctx tcLevel (level + 1) (childSt ctx level rs tc rs.lab[tc + o']!) targets key) (fuel level numcells : Nat) (st : SearchSt n) (targets : List Nat) (key : Key n) : P level (refine ctx level st.lab st.ptn st.active numcells) targets key → st.firstlab.size = n → st.firstlab.toList.Perm (List.range n) → Matches ctx level st targets key → HasLeaf ctx tcLevel level (refine ctx level st.lab st.ptn st.active numcells) targets key → st.eqlevFirst = level - 1 → st.needshortprune = false → st.gcaFirst < level → level ≤ n → n < level + fuel → have result := otherNode ctx inf tcLevel fuel level numcells st; result.fst = Int.ofNat st.gcaFirst ∧ LabelCarrier ctx st.firstlab result.snd.lab result.snd.genTrace

If a matching reference can be continued through every target child, the executable's first descent emits its carrier and returns to the first guide. This common induction serves both cheap and uniform subtrees.