We prove that no strongly regular graph with parameters (476,133,60,28) exists, and hence none with the complementary parameters (476,342,236,270). Brouwer's table lists this parameter set as open, and Koolen and Gebremichel list it among the twelve open primitive parameter sets with smallest eigenvalue −3, v > 276 and μ ∉ {6,9}; the result confirms one more case of their conjecture. No symmetry is assumed. The matrix A + 3I + J is positive semidefinite of rank 35, so the vertices span an even lattice of rank 35; let N be a maximal even overlattice. We prove by hand that the discriminant form of N is one of exactly two forms on Z/4 ⊕ Z/19; the proof combines Milgram's formula with a parity condition satisfied by the class of the normalized sum y of the vertex vectors. We prove an elementary counting lemma: every root of N is orthogonal to y, and if R₀ is the set of roots and S₄ the set of norm-4 vectors of N having the same inner product with y as the vertex vectors, then 38|R₀| ≤ 3(|S₄| − 476). For each form we glue N to explicit lattices of rank 5 and determinant 76, obtaining even unimodular lattices of rank 40; the harmonic theta series of degrees 0, 2 and 6 give linear equations in the numbers of vectors of each type in the shells of norm 2 and 4. Together with the counting lemma and the 63308 differences of adjacent vertices these equations are infeasible, as shown by exact rational Farkas certificates with 200 and 406 multipliers. The counting lemma is load-bearing: without it both systems are feasible. The proof is computer-assisted in the admissibility of vector types and in the two certificates. Every vector type omitted from the systems is rejected by an elementary test (moments, a quadratic bound, and a subset-sum test of the local identity); the paper lists all 337 omitted types with the reason for each. The certificates are checked by short exact programs (Python, exact rational arithmetic, no linear-programming solver) included in the data archive. The exclusion of both forms was independently re-derived by a blind audit carried out by a separate AI session with its own code, its own admissibility decider, its own row builders over all glue lattices and all gluings, and an exact simplex; a further separate AI referee session with its own code re-checked the hand proofs, the certificates, the harmonic rows and every type exclusion.
No takes yet. Share an insight, caveat, or question.
Anton Koval (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: