theorem Hex.GraphIso.Nauty.Generation.uniform_reference {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells : Nat} {st : SearchSt n} {targets : List Nat} {key : Key n} (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hT : TreeOk ctx level (refine ctx level st.lab st.ptn st.active numcells)) (hU : Uniform ctx tcLevel level (refine ctx level st.lab st.ptn st.active numcells) targets key) (hsize : st.firstlab.size = n) (hperm : st.firstlab.toList.Perm (List.range n)) (hm : Matches ctx level st targets key) (hlevel : st.eqlevFirst = level - 1) (hclear : st.needshortprune = false) (hguide : st.gcaFirst < level) (hfuel : 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

A valid uniform subtree whose key matches the first reference emits a carrier on its first descent. Leaf existence is derived from validity, so uniformity is never used vacuously.