theorem Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf.small {n : Nat} {G : SparseGraph n} {tcLevel level : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} (h : HasLeaf G tcLevel level st targets key) (hr : RefineSt.Ready G level st) (hshape : NodeShape n level st.ptn) : Uniform G tcLevel level st targets key

Every selected descent below a native cheap-shaped node has the same full key and targets. True cell-stabilizer transitivity transports literal child calls with independent bounded scratch; no generated-group completeness or dense execution is used.