The Bannai–Munemasa–Venkov lattice method for strongly regular graphs: a uniform discriminant-form condition and new nonexistence results

Bannai, Munemasa and Venkov, and later Nebe and Venkov, excluded tight spherical designs, among them strongly regular graphs of a special kind, by studying the lattice spanned by the design: they bound its discriminant group, pass to an even (over)lattice, and compare Gauss sums by the Milgram–Braun formula. We extend this method to arbitrary strongly regular graphs with integral eigenvalues. For an integral representation G = b(A − ρI) + cJ that is positive semidefinite with even diagonal, an elementary identity for dual vectors ties every class of the discriminant form of a maximal even overlattice to the class of a rescaled sum of the vertex vectors. This gives a necessary condition on the parameters (v, k, λ, μ) alone: a finite quadratic module with a short list of properties must exist. Its simplest case applies the textbook congruence det ≡ (−1)^(n/2) (mod 4) for even lattices of odd determinant to the centred representation. A sweep of Brouwer's table (v ≤ 1300) finds 70 complementary pairs of parameter sets listed as open that fail the condition, among them (96,35,10,14), the triangle-free set (176,25,0,4) and (169,42,5,12). The grade of evidence is given for each row: 28 pairs are excluded by hand, the other 42 by exact finite computations repeated by at least two independent programs. No existing parameter set of the table with v ≤ 1300 fails in any representation tested, real graphs satisfy every condition with their actual discriminant forms, and the method gives short independent second proofs of the known nonexistence of srg(75,32,10,16) and srg(289,54,1,12). The simplest case also yields an infinite family: if q is a power of a prime p ≡ 1 (mod 4) and m is odd, there is no strongly regular graph with the parameters (q², m(q+1), −q + m² + 3m, m(m+1)) of the negative-Latin-square type NL_m(q). This family, the parity case and the nonexistence of srg(169,42,5,12) are formalized in Lean 4 with Mathlib (https://github.com/tonykoval/srg-parity-lean). The deciders (five implementations, Python standard library only), the scan outputs, the controls and the table generator are in the data archive.