theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.uniform {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel last : Nat} {f : Frame n} {leaf : State n} {parents : Parents n} (h : FirstInput G tcLevel f parents) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel f.level f.numcells f.entry last leaf) (hf : n + 1 ≤ f.level + fuel) (hsame : (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).snd.allsamelevel ≤ f.level) : ∃ (targets : List Nat), ∃ (key : Key n), Generation.Uniform G.graph tcLevel f.level (State.refined (Graph.ofGraph G.graph) f.level f.numcells f.entry) targets key

The actual all-same boundary certifies every native leaf, including its target sequence and all refinement codes. The induction follows the guiding child and uses the actual sweep's counted checked carriers; it does not assume automorphism-generation completeness.