New lower bounds for the size of spherical designs

Let N(S^{n−1}, t) be the smallest number of points of a spherical t-design on S^{n−1}, with equal weights. We show that there is no spherical 4-design with 21 points on S^4, no spherical 6-design with 33 points on S^3, no spherical 6-design with 54 or 55 points on S^4, and no spherical 7-design with 42 points on S^3. So N(S^4, 4) ≥ 22, N(S^3, 6) ≥ 34, N(S^4, 6) ≥ 56 and N(S^3, 7) ≥ 43. The best published lower bounds we found are 21, 32, 54 (Boyvalenkov and Nikova, 1998) and 41 (Delsarte–Goethals–Seidel with Bannai–Damerell). The smallest known designs in the first, second and fourth cases have 29 points (Hardin and Sloane, 1992), 42 and 48 points (Sloane, Hardin and Cara, 2003). Version 2 adds Theorem 3 (S^4, t = 6) and Theorem 4 (S^3, t = 7); version 1 had Theorems 1 and 2. The Theorem 4 certificate has thin margins (about 1e-4), all decided in exact arithmetic. Each proof is an exact rational certificate for a three-point linear program in which the triple moments are fixed by conditioning on two design points (the method of our earlier note, doi:10.5281/zenodo.23615049). Positivity of the three-variable part on the Gram region is proved by exact integer Bernstein subdivision. The supplement contains the five certificates, two separately written exact checkers, tamper tests, controls on known designs (a 160-point design and a 640-point 7-design on S^4; the 600-cell and two 24-cells on S^3), and the literature check. As far as we checked, all four bounds are new; pointers to earlier work are welcome. AI use: the computations, the certificates, the checkers and the text were produced with Claude (Anthropic) under the author's direction; the second checker was written by a separate session of the same AI system, which is not independent human review. Not yet peer reviewed. Contact: [email protected].