theorem Hex.GraphIso.Nauty.Generation.first_uniform {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 → (firstPathNode ctx (n + 2) tcLevel fuel level numcells st).snd.allsamelevel ≤ level → ∃ (targets : List Nat), ∃ (key : Key n), Uniform ctx tcLevel level (refine ctx level st.lab st.ptn st.active numcells) targets key

When the first descent lowers its all-same boundary to the current frame, every leaf below that frame has the same codes, target hints, and adjacency rows. The proof follows the actual orbit counter.