# Nonexistence of a Strongly Regular Graph with Parameters (266,45,0,9): A Certificate-Free Lean Proof

> A fully formal Lean 4 proof shows no strongly regular graph with parameters (266, 45, 0, 9) exists, using lattice and design arguments without external certificates.

- **Source:** [arXiv](https://arxiv.org/abs/2609.08319)
- **Published:** 2026-09-12
- **Permalink:** https://picx.dev/p/Y1X2VL
- **Whiteboard:** https://picx.dev/p/Y1X2VL/image

## Summary

## 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:

| Type | $b$ | $\|a_y\|^2$ | $\|e_y\|^2$ |
|------|-----|-------------|-------------|
| I | 9 | 9/4 | 0 |
| II | 1 | 11/12 | 4/3 |

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:

| $C$ | 3-primary part | 5-primary part | det $C$ |
|-----|----------------|----------------|---------|
| $E_6$ | $\langle 2/3 \rangle$ | 0 | 3 |
| $H_6$ | $\langle 2/3 \rangle$ | $\langle 2/5 \rangle$ | 15 |
| $A_2 \perp A_4$ | $\langle 4/3 \rangle$ | $\langle 4/5 \rangle$ | 15 |
| $A_4 \perp Q_{15}$ | $\langle 4/3 \rangle$ | $\langle 2/5 \rangle \perp \langle 4/5 \rangle$ | 75 |

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

| | Lean project build | nanoda check |
|---|---|---|
| Wall time | 884.17 s | 24.47 s |
| Largest child-process RSS | 3.85 GiB | 1.81 GiB |
| Declarations checked | — | 77,402 |

## 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.

---

_Markdown view of https://picx.dev/p/Y1X2VL, served by PicX — AI-generated visual whiteboard summaries of research papers._