theorem Hex.GraphIso.Nauty.Generation.first_path {n k : Nat} {G : Colored n k} {ctx : Ctx n} (tcLevel : Nat) (hg : ctx.g = rowsOf G) (fuel level numcells : Nat) (codes : List Nat) (st : SearchSt n) (trail : FrameTrail) : FirstInv G ctx level codes numcells 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 → 1 ≤ level → level = codes.length + 1 → st.firsttc.size = n + 2 → n + 2 < level + fuel → ∃ (targets : List Nat), ∃ (key : Key n), RefPath ctx tcLevel (firstPathNode ctx (n + 2) tcLevel fuel level numcells st).snd.allsamelevel level (refine ctx level st.lab st.ptn st.active numcells) targets key ∧ Matches ctx level (firstPathNode ctx (n + 2) tcLevel fuel level numcells st).snd targets key

The actual first descent installs a reference path carrying the uniformity guarantee at its final all-same boundary.