A one-sided quartic bound for spherical codes and the optimality of Kerdock codes

Let A(d,s) be the largest number of points on the unit sphere in R^d with pairwise inner products at most s. We prove that A(d,s) ≤ 2d(d+2)(1−s²)/(3−(d+2)s²) for d ≥ 4096 and 0 < s² ≤ 1/d + 1/(100d²). At s = d^{−1/2} the bound equals d(d+2) and is attained exactly by antipodal lifts of complete systems of real mutually unbiased bases. Together with the results of Cohn, de Laat and Leijenhorst for 16 ≤ d ≤ 1024, this shows that the Kerdock spherical codes and the binary Kerdock codes are optimal in every dimension 4^k, k ≥ 2. The proof also gives a stability estimate and an asymptotic version for |s^{−2} − d| = o(d^{1/8}). Files: the paper (PDF) and a Lean 4 supplement formalizing the main cardinality bound, the stability estimate, the equality conditions and the binary bound. See the README inside the archive.