Nonexistence of a Strongly Regular Graph with Parameters (266,45,0,9): A Certificate-Free Lean Proof
Abstract
We prove that no strongly regular graph with parameters $(266, 45, 0, 9)$ exists. The proof is formalized in Lean 4 and Mathlib without external infeasibility certificates or assumed classification theorems. A hypothetical graph gives a rank-$12$ integral Gram lattice with an integral centroid. A Lorentzian change of form, a marked D7 gluing, and an explicit rank-six complement produce a positive-definite even unimodular lattice of rank $24$, together with the original indexed family of $220$ vectors. Harmonic theta identities and a root-isolation inequality force the root system A11 ⊥ D7 ⊥ E6. First and second moments then exclude the possible complements: the final case reduces to an impossible binary projection identity 4x + 4y − 2z = 50. A type-A subcase is closed by a separate classification-free proof of the known nonexistence of a quasi-symmetric $2−(56, 12, 9)$ design with intersections $0, 3$. That argument constructs a Krein graph and forces a Steiner $3−(12, 4, 1)$ design, contradicting its replication equation. The formal theorem depends only on the three standard Lean axioms and has also been checked independently with nanoda. The archived formalization is release v2.0.0.
Related
- Nonexistence of strongly regular graphs via multipoint spherical semidefinite bounds
- Nonexistence of Strongly Regular Graphs via Gegenbauer Positivity and SRG Counting
- Coherent configuration on 3-uniform hypergraph over strongly regular graph
- An Induced Subgraph Paradigm for Strongly Regular Graph Constructions
- Strongly regular graph, strongly polynomial sequences, and two-level polynomials
BibTeX
@misc{akiyama2026nonexistence,
title = {{Nonexistence of a Strongly Regular Graph with Parameters (266,45,0,9): A Certificate-Free Lean Proof}},
author = {Kay Akiyama},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.08319},
eprint = {2609.08319},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.08319},
}
RIS
TY - UNPB
TI - Nonexistence of a Strongly Regular Graph with Parameters (266,45,0,9): A Certificate-Free Lean Proof
AU - Kay Akiyama
PY - 2026
DA - 2026/09/08
PB - arXiv
DO - 10.48550/arxiv.2609.08319
UR - https://arxiv.org/abs/2609.08319
AB - We prove that no strongly regular graph with parameters $(266, 45, 0, 9)$ exists. The proof is formalized in Lean 4 and Mathlib without external infeasibility certificates or assumed classification theorems. A hypothetical graph gives a rank-$12$ integral Gram lattice with an integral centroid. A Lorentzian change of form, a marked D_7 gluing, and an explicit rank-six complement produce a positive-definite even unimodular lattice of rank $24$, together with the original indexed family of $220$ vectors. Harmonic theta identities and a root-isolation inequality force the root system A_11 ⊥ D_7 ⊥ E_6. First and second moments then exclude the possible complements: the final case reduces to an impossible binary projection identity 4x + 4y − 2z = 50. A type-A subcase is closed by a separate classification-free proof of the known nonexistence of a quasi-symmetric $2−(56, 12, 9)$ design with intersections $0, 3$. That argument constructs a Krein graph and forces a Steiner $3−(12, 4, 1)$ design, contradicting its replication equation. The formal theorem depends only on the three standard Lean axioms and has also been checked independently with nanoda. The archived formalization is release v2.0.0.
ER -