Stable Levenshtein Spheres for Run Strings: Exact Formulas, Certification, and Polynomial Structure

Exact sizes of Levenshtein spheres are hard to compute because different edit scripts can produce the same string. We study run strings u=x1n1…xmnm in the stable regime, where every run length is at least the radius r. For r=2 we prove a closed formula for |SL(u,2)| for every m≥2: the layers of output length n−1, n and n+1 are identified with explicit sets of strings described through longest common prefixes and suffixes, and the layers of length n±2 follow from deletion and insertion counts. For r=3 we give a computer-assisted proof of a closed formula for 2≤m≤7. The proof rests on a certification method: a banded edit-distance automaton shows that the sphere size is a polynomial of bounded degree in the run lengths and in Q=q−1, where q is the alphabet size, so a candidate formula is proved by exact evaluation on an explicit finite set of profiles. In all proved cases the coefficients of the polynomial in Q are polynomials in the invariants S1, P2, P3, B1, E1, E2, and n1nm of the run profile. We state conjectured formulas, supported by exact enumeration, for r=3 with m≥8 and for r=4 with five runs, formulate a general template conjecture, and give an algorithm, based on exact enumeration, interpolation, and invariant fitting that discovers such formulas.