Summary (Overview)

• Main Result: The paper proves that no strongly regular graph with parameters (266, 45, 0, 9) exists, providing a complete formal proof in Lean 4 and Mathlib.
• Novel Approach: The proof uses a lattice-theoretic construction — a hypothetical graph yields a rank-12 integral Gram lattice, which is then completed to a positive-definite even unimodular rank-24 lattice with a marked $D_7$ factor.
• Certificate-Free: Unlike earlier drafts, the proof avoids external infeasibility certificates, shell enumerations, and classification theorems, relying only on the three standard Lean axioms.
• Two-Branch Structure: The main argument splits into a lattice/binary-projection branch and a design-theoretic branch (excluding a quasi-symmetric 2-(56, 12, 9) design).
• Verification: The formalization is independently checked with nanoda, with the archived release at DOI 10.5281/zenodo.22509839 (v2.0.0).

Introduction and Theoretical Foundation

A strongly regular graph with parameters $(v, k, \lambda, \mu)$ is a finite simple graph with $v$ vertices where each vertex has $k$ neighbours, adjacent vertices share $\lambda$ common neighbours, and distinct nonadjacent vertices share $\mu$ common neighbours. For the parameters (266, 45, 0, 9), the adjacency spectrum would be:

$$45^{(1)}, \qquad 3^{(209)}, \qquad (-12)^{(56)}$$

Key theoretical tools:

• The Hoffman ratio bound for a coclique is 56.
• Euclidean representations and Gram matrices are standard tools for studying strongly regular graphs.
• Prior results excluded 5-chromatic graphs and graphs containing a Delsarte coclique of size 56, but this proof makes no such assumptions.

The mathematical mechanism proceeds through the chain:

$$\text{SRG}(266, 45, 0, 9) \Rightarrow \text{integral centroid and rank-11 tight frame} \Rightarrow \text{marked even unimodular rank-24 lattice}$$ $$\Rightarrow A_{11} \perp D_7 \perp E_6 \Rightarrow \text{component masses } 275, 220 \Rightarrow \text{binary projection obstruction}$$

Methodology

1. Local Gram Lattice Construction

Fix a vertex $o$ with neighbourhood $X$ (45 vertices) and $Y = V(\Gamma) \setminus (\{o\} \cup X)$ (220 vertices). The key object is the matrix:

$$L = 9I + 3J - S - 3H$$

where $S$ is the incidence matrix product and $H$ is the induced graph on $Y$. This yields:

$$L\mathbf{1} = 165\mathbf{1}, \qquad L^2 = 45L + 90J$$

The lattice $\Lambda$ (quotient of $\mathbb{Z}^Y$ by the radical of $L$) is positive-definite of rank 12.

Integral Centroid (Proposition 2.3): There exists $c \in \Lambda$ such that:

$$\sum_{y \in Y} g_y = 11c, \qquad \langle c, g_y \rangle = 15, \qquad \|c\|^2 = 300$$

2. Marked Completion in Dimension 24

A Lorentzian change of form gives signature (11,1) with:

$$[g_y, g_z] = L_{yz} - 1, \quad [\rho, g_y] = -1, \quad [\rho, \rho] = -4$$

The vectors $u_y = g_y - \rho/4$ satisfy:

$$\|u_y\|^2 = \frac{9}{4}, \quad \sum_y u_y = 0, \quad \sum_y \langle v, u_y\rangle\langle w, u_y\rangle = 45\langle v, w\rangle$$

A marked $D_7$ gluing produces the even lattice $N = (T \perp D_7) + \mathbb{Z}(u_{y_0}, s)$ where $s = (1/2, \ldots, 1/2)$. The completion yields a positive-definite even unimodular lattice $\mathcal{L}$ of rank 24.

3. Root System Determination

Root Isolation Lemma: Every root of $\mathcal{L}$ is either a root of the marked $D_7$ or orthogonal to its span. This follows from a root-isolation inequality: if $0 < \|a\|^2 < 2$ for the $D_7^*$ component, then $\sum_y \langle v, u_y\rangle^2 \geq 220 \cdot d/4$ but also $\leq 45d$, giving $220 \leq 180$, a contradiction.

Venkov's Harmonic Root Identity:

$$\sum_{r \in R(\mathcal{L})} \langle r, v\rangle\langle r, w\rangle = \frac{|R(\mathcal{L})|}{12}\langle v, w\rangle$$

This forces the root system to be $A_{11} \perp D_7 \perp E_6$ with 288 roots.

4. Design-Theoretic Branch

The type-A subcase constructs a quasi-symmetric 2-(56, 12, 9) design, which is excluded via:

• Local triangular graphs $T(11)$
• Ternary self-orthogonality gluing to a canonical biplane
• Construction of a Krein graph SRG(324, 57, 0, 12)
• Forcing a Steiner 3-(12, 4, 1) design, contradicting $3r = 55$

Empirical Validation / Results

Component Masses

After normalization, the 220 indices split into two types:

First moments give:

$$n_0 = 55, \quad n_1 = 165, \quad \sum_y \|a_y\|^2 = 275, \quad \sum_y \|e_y\|^2 = 220$$

Complement Elimination

Trace bounds eliminate three of the four possible rank-six complements:

Only $C = A_4 \perp Q_{15}$ survives, leading to the final binary projection trace:

$$4x + 4y - 2z = 50$$

with $x, y \in \{0, 4, 6, 12\}$ and $z^2 \leq xy$. The only solution up to interchange is $x = y = 6$, giving $z = -1$, contradicting $3 \mid z$.

Verification Metrics

Theoretical and Practical Implications

• Methodological Innovation: The proof demonstrates that preserving local incidence data through lattice constructions can replace large certificate-based searches. The "extra dimensions" of the rank-24 completion impose identities on the original configuration.
• Formal Verification: The proof is fully formalized in Lean 4 with only the three standard axioms (propext, Classical.choice, Quot.sound), checked independently by two different proof checkers.
• Classification-Free: The design branch avoids the Hall–Connor embedding theorem and biplane classifications, replacing them with local graph identities and divisibility arguments.
• Recovery of Known Results: Together with the classical subconstituent theorem, the result recovers the known nonexistence of SRG(324, 57, 0, 12).

Conclusion

The paper establishes the nonexistence of a strongly regular graph with parameters (266, 45, 0, 9) through a "certificate-free" proof that preserves a local frame while changing its ambient geometry. The integral centroid provides the arithmetic foundation for a marked even unimodular completion; a root-isolation gap and vanishing harmonic theta series determine the root system $A_{11} \perp D_7 \perp E_6$; first moments fix shell-type counts; and second moments bound remaining projections, culminating in the impossible binary projection identity $4x + 4y - 2z = 50$.

The design branch follows the same principle: compatibility across local triangular structures replaces separate searches, and a forced Steiner completion ends in the elementary divisibility contradiction $3r = 55$. The result is an end-to-end formal proof with no external infeasibility data, verified in Lean 4 and independently checked with nanoda.