There is no strongly regular graph with parameters (154,72,26,40)

We prove that no strongly regular graph with parameters (154,72,26,40) exists; Brouwer's table lists this parameter set as open. No symmetry is assumed. The matrix −A + 2I + 2J is positive semidefinite of rank 22, so the vertices span an even lattice. For every dual vector of a maximal even overlattice N, the inner products with the vertices form an integer vector z with prescribed sum and sum of squares and with Az = −16z + 4ℓ𝟏 (𝟏 the all-ones vector). Elementary counting turns this into a list of forbidden dual vectors, each with a short certificate. Milgram's formula leaves two genera for N, of determinants 51 and 204. In determinant 51, N glues into the Niemeier lattice A_1^24, and one vector built from a dodecad of the Golay code always projects to a dual vector of the forbidden norm 20/17. In determinant 204, N glues into an odd unimodular lattice U of dimension 23 without vectors of norm 1. If U has roots, an identity between its roots and its characteristic vectors of norm 7 gives a contradiction in a few lines. If not, its 4600 vectors of norm 3 form a spherical 7-design, and a polynomial of degree 6 that vanishes on all of them has nonzero sum over them. The proof is by hand, apart from the bookkeeping of a printed table of elementary certificates. It does not use the classification of the odd unimodular lattices of dimension 23; the one identity taken from a companion paper is proved again in an appendix. The arithmetic core of the proof (all forbidden dual vectors with their printed certificates, the pinning lemma, both cases in dimension 23 and the dodecad witness) has been formally verified in Lean 4 with Mathlib, conditional on the stated lattice-theoretic inputs.