theorem Hex.GraphIso.Nauty.Generation.other_reference {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel : Nat} (hg : ctx.g = rowsOf G) (hinf : inf = n + 2) (fuel level numcells : Nat) (codes bs fs : List Nat) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) (boundary : Nat) (targets : List Nat) (key : Key n) : 2 ≤ level → level = codes.length + 1 → n + 2 < level + fuel → NodeInv G ctx tcLevel level codes bs fs numcells st best trail → Live ctx level st trail → PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st → st.noncheaplevel ≤ level → CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells) → OrbSound (OrbConn st.genTrace.toList n) st.orbits n → st.cosetindex < n → (∀ (b : Key n), best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b) → RefPath ctx tcLevel boundary level (refine ctx level st.lab st.ptn st.active numcells) targets key → Matches ctx level st targets key → st.eqlevFirst = level - 1 → boundary ≤ st.allsamelevel → RefReturn ctx (otherNode ctx inf tcLevel fuel level numcells st).snd (otherNode ctx inf tcLevel fuel level numcells st).fst

Every valid off-path visit containing the stored first reference returns automorphism evidence. Uniform and cheap subtrees use their first descent; the remaining nodes use verified coverage of the actual sweep.