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

Kay Akiyama

Date: 8 September 2026

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 $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}\perp D_{7}\perp 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.

Key words and phrases:

strongly regular graph, integral lattice, even unimodular lattice, harmonic theta series, quasi-symmetric design, formal proof, Lean

2020 Mathematics Subject Classification

Primary 05E30; Secondary 05C50, 05B05, 11H55, 68V20

1. Introduction

A finite simple graph is strongly regular with parameters $(v,k,\lambda,\mu)$ if it has $v$ vertices, each vertex has $k$ neighbours, adjacent vertices have $\lambda$ common neighbours, and distinct nonadjacent vertices have $\mu$ common neighbours. Standard spectral and divisibility conditions leave many feasible parameter sets whose existence is a separate question; see [10] and Brouwer’s online parameter tables [8].

Theorem 1.1.

No strongly regular graph has parameters $(266,45,0,9)$ .

For these parameters the adjacency spectrum would be

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

and the Hoffman ratio bound for a coclique is $56$ [9, Section 3.5]. Earlier results exclude a $5$ -chromatic graph with these parameters [18, Theorem 7.3, p. 3089] and, through the associated quasi-symmetric design, a graph containing a Delsarte coclique of size $56$ [1, 25]. Theorem 1.1 makes neither assumption. Its contribution is the exclusion of an arbitrary hypothetical graph by a lattice construction retaining its local incidence data.

Remark 1.2.

An earlier unpublished draft, synchronized with release v1.1.0, used rank- $15$ odd unimodular hosts and finite infeasibility certificates. The present argument retains the local Gram construction and integral centroid, but replaces those exclusions by a marked rank- $24$ completion and moment identities.

The mathematical mechanism

Fix a vertex of the hypothetical graph. Its second subconstituent has $220$ vertices, which index norm- $3$ vectors in a rank- $12$ lattice. Subtracting the centroid direction gives a zero-sum tight frame in dimension $11$ . The arithmetic of this frame permits a marked completion in dimension $24$ . The main route is

\begin{gathered}\operatorname{SRG}(266,45,0,9)\ \Longrightarrow\ \text{integral centroid and rank-$11$ tight frame}\\ \Longrightarrow\ \text{marked even unimodular rank-$24$ lattice}\\ \Longrightarrow\ A_{11}\perp D_{7}\perp E_{6}\ \Longrightarrow\ \text{component masses }275,220\\ \Longrightarrow\ \text{binary projection obstruction}.\end{gathered}

One branch forces a binary weight-three factorization of the original Gram matrix. It is excluded independently by

\begin{gathered}\text{quasi-symmetric }2\text{-}(56,12,9),\ \{0,3\}\\ \Longrightarrow\ \text{canonical biplane and a }3\text{-}(57,12,2)\text{ design}\\ \Longrightarrow\ \text{structured Krein graph on }324\text{ vertices}\\ \Longrightarrow\ \text{Steiner }3\text{-}(12,4,1)\ \Longrightarrow\ 3r=55.\end{gathered}

The extra dimensions are useful because they impose identities on the same configuration that came from the graph. An unmarked existence statement about a lattice would not be sufficient. In particular, the $220$ indices are never replaced by a set of distinct projected vectors.

Prior results and scope

The quasi-symmetric-design nonexistence statement is due to Munemasa and Tonchev [25]; it is not claimed as new. Their proof uses the Hall–Connor embedding theorem and the classification of biplanes on $56$ points [20, 22], and builds on the ternary-code computations of Key and Tonchev [23]. Our internal proof constructs a compatible biplane from the hypothetical design and closes the argument by local graph identities, without using that classification.

Gavrilyuk and Makhnev [19] proved that no graph with parameters $(324,57,0,12)$ exists. Section 6 establishes the structured special case needed here, not a new general $324$ -vertex theorem. Conversely, the classical subconstituent theorem [11, 4] implies that every hypothetical $\operatorname{SRG}(324,57,0,12)$ has second subconstituents with parameters $(266,45,0,9)$ . Together with Theorem 1.1, this recovers the known general $324$ -vertex nonexistence. This last implication is literature-level context, not an additional formalized corollary or an input to our proof.

Chen, Makhnev, and Nirova [13] characterize the existence of a triangle-free Krein graph $\operatorname{Kre}(r)$ by the existence of a graph $\operatorname{Kre}(r)^{\prime}$ with the second-subconstituent parameters that is also the complement of a quasi-symmetric design’s block graph. For $r=3$ these are the $324$ - and $266$ -vertex parameter sets above. The block-graph realization is an additional hypothesis; their result does not extend an arbitrary $\operatorname{SRG}(266,45,0,9)$ to a $324$ -vertex graph. Section 6 supplies such a realization only in the design branch.

Euclidean representations and Gram matrices are standard tools in the study of strongly regular graphs [10, Section 1.3.5]. Direct precedents for nonexistence arguments using these tools are Bondarenko, Prymak, and Radchenko’s exclusion of $(76,30,8,14)$ [5] and Bondarenko et al.’s exclusion of $(460,153,32,60)$ [6]. Both combine Euclidean representations and Gram-matrix restrictions with bounds on $4$ -cliques; the former also uses low-dimensional orthogonal projections. Here the additional ingredient is an integral marked completion retaining the original indexed configuration, to which root and moment identities apply. We use standard terminology for lattices and root systems [15]. We write squared norms as $\lVert v\rVert^{2}$ ; as usual in lattice terminology, a vector of norm $m$ means $\lVert v\rVert^{2}=m$ . No classification of rank- $24$ even unimodular lattices is invoked. The required ADE analysis and harmonic theta argument are proved in the formal development. The paper gives their mathematical content and the reductions they support; Appendix A identifies the corresponding formal statements.

2. The local Gram lattice

Assume that $\Gamma$ is a hypothetical graph in Theorem 1.1. Its adjacency matrix $A$ satisfies

A^{2}=36I-9A+9J.

(1)

The spectrum stated in the introduction follows by restricting this identity to $\mathbf{1}^{\perp}$ and using the trace. Fix a vertex $o$ and put $X=\Gamma(o)$ and $Y=V(\Gamma)\setminus(\{o\}\cup X)$ . Then $|X|=45$ , $|Y|=220$ , and $X$ is independent. For $y\in Y$ let $B_{y}=\Gamma(y)\cap X$ .

Lemma 2.1.

The indexed blocks $(B_{y})_{y\in Y}$ form a $2$ - $(45,9,8)$ design with replication number $44$ . The induced graph $H=\Gamma[Y]$ is $36$ -regular. Writing $M$ for the $45\times 220$ incidence matrix and $S=M^{\mathsf{T}}M$ , one has

$\displaystyle S\mathbf{1}$	$\displaystyle=396\mathbf{1},$	$\displaystyle H\mathbf{1}$	$\displaystyle=36\mathbf{1},$
$\displaystyle S^{2}$	$\displaystyle=36S+648J,$	$\displaystyle SH=HS$	$\displaystyle=81J-9S,$	(2)
$\displaystyle H^{2}$	$\displaystyle=36I+9J-S-9H.$

Proof.

A vertex of $Y$ has $9$ common neighbours with $o$ , so $|B_{y}|=9$ . Each point of $X$ has $44$ neighbours in $Y$ . Two distinct points of $X$ have $8$ common neighbours in $Y$ , the ninth being $o$ . Thus $MM^{\mathsf{T}}=36I+8J$ , giving the identity for $S^{2}$ . The other identities are the corresponding blocks of (1). ∎

Define

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

(3)

Its diagonal is $3$ , and for $y\neq z$ its entry is $0$ if $y\sim_{H}z$ , and $3-|B_{y}\cap B_{z}|$ otherwise. Substitution in (2) gives

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

(4)

Consequently $L$ is positive semidefinite, with nonzero eigenvalues $165^{(1)}$ and $45^{(11)}$ . Indeed, the possible eigenvalues on $\mathbf{1}^{\perp}$ are $0,45$ , and $\operatorname{tr}L=660$ fixes the multiplicity. Let $\Lambda$ be the quotient of $\mathbb{Z}^{Y}$ by its integral radical for $L$ , and let $g_{y}$ be the image of the $y$ th standard basis vector. This is a positive-definite integral lattice of rank $12$ , with $\langle g_{y},g_{z}\rangle=L_{yz}$ .

Lemma 2.2.

For $y\neq z$ one has $|B_{y}\cap B_{z}|\leq 3$ . In particular $L_{yz}\in\{0,1,2,3\}$ .

Proof.

The symmetric matrix $Q=4L-3J$ satisfies $Q^{2}=180Q$ , so its eigenvalues are $0$ or $180$ and it is positive semidefinite. Its diagonal entries are $Q_{yy}=9$ . If $y,z$ are nonadjacent and $t=|B_{y}\cap B_{z}|$ , the corresponding principal two-by-two minor gives $|9-4t|\leq 9$ , hence $t\leq 4$ .

To exclude $t=4$ , put $K_{0}=L-J=(k_{yz})$ . Then

K_{0}^{2}=45K_{0}+25J,\qquad K_{0}\mathbf{1}=-55\mathbf{1},\qquad k_{yy}=2.

All off-diagonal entries of $K_{0}$ are integers between $-2$ and $2$ . For $\phi(a)=a(a+1)/2$ and $w\notin\{y,z\}$ ,

\phi(k_{yw})+\phi(k_{zw})+k_{yw}k_{zw}-H_{yw}H_{zw}\geq 0.

Without the last term the expression is $\phi(k_{yw}+k_{zw})\geq 0$ . If the last term is $1$ , both $k$ -entries are $-1$ and the expression is zero. Under $k_{yz}=-2$ , set $Y^{\prime}=Y\setminus\{y,z\}$ . The row and diagonal square identities give

\sum_{w\in Y^{\prime}}k_{yw}=-55,\qquad\sum_{w\in Y^{\prime}}k_{yw}^{2}=115-2^{2}-(-2)^{2}=107.

Hence $\sum_{w\in Y^{\prime}}\phi(k_{yw})=(107-55)/2=26$ , and likewise for $z$ . The off-diagonal identity $(K_{0}^{2})_{yz}=-65$ gives $\sum_{w\in Y^{\prime}}k_{yw}k_{zw}=-65+8=-57$ . There are $9-4=5$ common neighbours in $H$ . Summation therefore gives $0\leq 26+26-57-5=-10$ . ∎

Proposition 2.3 (Integral centroid).

There is $c\in\Lambda$ such that

\sum_{y\in Y}g_{y}=11c,\qquad\langle c,g_{y}\rangle=15,\qquad\lVert c\rVert^{2}=300.

(5)

Proof.

Reduce $L$ modulo $11$ and write $\bar{L}$ for the resulting matrix. Its rank is at most its rational rank, namely $12$ . Equation (4) gives $\bar{L}^{2}=\bar{L}+2J$ , $\bar{L}J=J\bar{L}=0$ , and $J^{2}=0$ . Thus $\bar{L}^{2}$ is idempotent. It is nonzero (its diagonal is $5$ ), and its trace is zero in $\mathbb{F}_{11}$ . Its rank is a positive multiple of $11$ , so it is $11$ . If $\bar{L}$ also had rank $11$ , its image would equal that of $\bar{L}^{2}$ . But the nonzero image of $\bar{L}^{2}-\bar{L}=2J$ lies both in that image and in the kernel of the idempotent $\bar{L}^{2}$ , a contradiction. Hence $\operatorname{rank}\bar{L}=12$ .

The integral radical is saturated. Its reduction injects into $\mathbb{F}_{11}^{Y}$ and has dimension $208$ , so it is the entire kernel of $\bar{L}$ . Since $\bar{L}\mathbf{1}=0$ , there is an integral radical vector $z$ with $z\equiv\mathbf{1}\pmod{11}$ . Writing $\mathbf{1}-z=11a$ gives $c=\sum_{y}a_{y}g_{y}$ . The remaining identities follow from the row sum of $L$ . ∎

Formal reference. SRG266/KernelReduction.lean

exists_integral_centroid.

3. A marked completion in dimension twenty-four

All rational spaces in this section are subsequently extended to real Euclidean spaces when orthogonal projection is used. The constructions and their lattice membership statements are first made over $\mathbb{Q}$ . The discriminant-form and gluing framework is standard [28, Section 1]. In particular, even overlattices correspond to isotropic subgroups of the discriminant form; their discriminant forms are the induced forms on the orthogonal quotients. We establish the instances needed below inside Lean.

3.1. The Lorentzian form and the tight frame

On $\Lambda\otimes\mathbb{Q}$ define

h(v)=\frac{\langle c,v\rangle}{15},\qquad[v,w]=\langle v,w\rangle-h(v)h(w),\qquad\rho=\frac{c}{5}.

This form has signature $(11,1)$ and

[g_{y},g_{z}]=L_{yz}-1,\quad[\rho,g_{y}]=-1,\quad[\rho,\rho]=-4,\quad[\rho,v]=-h(v).

(6)

The lattice $\Lambda+\mathbb{Z}\rho$ is even and integral for $[\ ,\ ]$ . Its dual quotient is killed by $45$ , as follows from the frame identity

\sum_{y}[v,g_{y}]g_{y}=45v-5h(v)c.

(7)

For $v=g_{z}$ , this identity follows by pairing both sides with each $g_{w}$ in the original positive-definite form and using $L^{2}=45L+90J$ and $\langle c,g_{w}\rangle=15$ ; it then extends by linearity because the $g_{z}$ span the space. Choose a maximal integral overlattice $P$ of this marked lattice. Since the dual quotient is killed by the odd integer $45$ , every such overlattice has odd index. For $v\in P$ , an odd multiple $nv$ lies in the original even lattice; thus $n^{2}[v,v]\in 2\mathbb{Z}$ , and integrality forces $[v,v]\in 2\mathbb{Z}$ . Consequently $P$ is even, and its discriminant group has no $2$ -primary part. By the overlattice–isotropic-subgroup correspondence, maximality makes its discriminant form anisotropic, and its discriminant group is killed by $15$ .

Put $U=\rho^{\perp}=\ker h$ and $T=P\cap U$ . The restriction of $[\ ,\ ]$ to $U$ is positive definite and agrees with the original form. Define

u_{y}=g_{y}-\frac{\rho}{4}=g_{y}-\frac{c}{20}.

(8)

These vectors belong to $T^{*}$ , lie in a single coset of $T$ , and satisfy

\lVert u_{y}\rVert^{2}=\frac{9}{4},\qquad\sum_{y}u_{y}=0,\qquad\sum_{y}\langle v,u_{y}\rangle\langle w,u_{y}\rangle=45\langle v,w\rangle\quad(v,w\in U).

(9)

In particular $\dim U=11$ and the vectors span $U$ . Their common class has order $4$ in $T^{*}/T$ , since $4u_{y}=4g_{y}-\rho\in T$ , while an integral multiple of $u_{y}$ can have even norm only if that multiple is divisible by $4$ . To see that this is the whole $2$ -primary part, note that $[\rho,g_{y}]=-1$ makes $\rho$ primitive in $P$ and gives $[\rho,P]=\mathbb{Z}$ . Thus the projection of $P$ onto $\mathbb{Q}\rho$ is $\tfrac{1}{4}\mathbb{Z}\rho$ , so $[P:T\perp\mathbb{Z}\rho]=4$ . Taking absolute Gram determinants yields

4|T^{*}/T|=4^{2}|P^{*}/P|,\qquad|T^{*}/T|=4|P^{*}/P|.

Since $|P^{*}/P|$ is odd, the $2$ -primary part of $T^{*}/T$ is precisely the cyclic group generated by the common class of the $u_{y}$ , of quadratic value $9/4$ modulo $2\mathbb{Z}$ .

Formal reference. SRG266/Completion/Perpendicular.lean

lorentzPerpGenerator_secondMoment.

3.2. The marked $D_{7}$

Use the coordinate lattice

D_{7}=\{a\in\mathbb{Z}^{7}:\textstyle\sum_{i}a_{i}\text{ is even}\},\qquad s=(1/2,\ldots,1/2).

Its spinor class has order $4$ and norm $7/4$ . Fix one index $y_{0}$ and form the even gluing

N=(T\perp D_{7})+\mathbb{Z}(u_{y_{0}},s)\subset U\perp\mathbb{Q}^{7}.

(10)

Because $u_{y}-u_{y_{0}}\in T$ , all the vectors $t_{y}=(u_{y},s)$ belong to $N$ . They have norm $4$ and

\langle t_{y},t_{z}\rangle=L_{yz}+1.

(11)

The order-four discriminant parts cancel. The remaining discriminant form has only $3$ - and $5$ -primary parts, inherited from the anisotropic discriminant form of $P$ .

Proposition 3.1 (Marked completion).

There is a positive-definite even unimodular lattice $\mathcal{L}$ in

(U\perp\mathbb{Q}^{7})\perp W,\qquad\dim W=6,

containing $N\perp C$ , where $C$ is one of the four lattices in Table 1. Moreover

\mathcal{L}\cap(U\perp\mathbb{Q}^{7})=N,\qquad\mathcal{L}\cap W=C,\qquad\mathcal{L}\cap\mathbb{Q}^{7}=D_{7}.

The $220$ specified vectors $(u_{y},s,0)$ belong to $\mathcal{L}$ .

Table 1. The four explicit rank-six complements. Quadratic values in the middle columns describe

\operatorname{disc}N

and are taken modulo

2\mathbb{Z}

. Angle brackets denote cyclic forms, and

0

denotes the trivial group.

$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$

Here $Q_{15}$ has Gram matrix $\left(\begin{smallmatrix}4&1\\ 1&4\end{smallmatrix}\right)$ . For an explicit description of $H_{6}$ , take $A_{5}\perp\mathbb{Z}e$ with $\lVert e\rVert^{2}=10$ and adjoin $(3\omega,e/2)$ , where $\omega$ generates $A_{5}^{*}/A_{5}$ and $\lVert\omega\rVert^{2}=5/6$ . This is an index-two even extension, of determinant $6\cdot 10/4=15$ ; it contains the displayed $A_{5}$ .

Proof of Proposition 3.1.

An anisotropic quadratic form over $\mathbb{F}_{3}$ or $\mathbb{F}_{5}$ has dimension at most two. Diagonalization leaves, at each prime, the trivial form, the two one-dimensional square classes, or the anisotropic binary form. The formal proof establishes these small normal forms directly, including the lifts of their generators and their norms modulo $2\mathbb{Z}$ .

One may first cancel each primary form by an explicit positive even lattice, without prescribing the final dimension. The forms and their cancelling models are listed in Table 2. Let $\omega_{n}\in A_{n}^{*}$ be an endpoint fundamental weight, of norm $n/(n+1)$ . Here $\Xi_{8}$ is the index-four extension of $A_{7}\perp\mathbb{Z}e$ , $\lVert e\rVert^{2}=10$ , obtained by adjoining $(2\omega_{7},e/2)$ . It has determinant $5$ . The lattice $\Xi_{4}$ is the index-three extension of $A_{2}\perp A_{2}(5)$ obtained by adjoining $(\omega_{2},\omega_{2})$ , where $A_{2}(5)$ denotes the form scaled by $5$ . It has determinant $25$ . Direct dual calculations verify the asserted cancellations.

Table 2. Positive even lattices whose discriminant forms are the negatives of the listed primary forms.

$p$	Primary form	Cancelling model	Rank
$3$	$0$	$0$	$0$
$3$	$\langle 2/3\rangle$	$E_{6}$	$6$
$3$	$\langle 4/3\rangle$	$A_{2}$	$2$
$3$	$\langle 2/3\rangle\perp\langle 2/3\rangle$	$A_{2}\perp A_{2}$	$4$
$5$	$0$	$0$	$0$
$5$	$\langle 2/5\rangle$	$\Xi_{8}$	$8$
$5$	$\langle 4/5\rangle$	$A_{4}$	$4$
$5$	$\langle 2/5\rangle\perp\langle 4/5\rangle$	$\Xi_{4}$	$4$

The resulting positive-definite even unimodular lattice must have rank divisible by $8$ ; see [17, Chapter 2]. Applied to the source rank $18$ , this leaves exactly the four pairs in Table 1. The rank divisibility is itself proved in the development, not assumed.

For each remaining pair, Table 1 supplies a rank-six lattice with the negative discriminant form. In particular, $H_{6}$ replaces the preliminary $E_{6}\perp\Xi_{8}$ , of rank $6+8=14$ , by a rank-six lattice with the same discriminant form. For the last pair, $A_{4}\perp Q_{15}$ replaces $A_{2}\perp\Xi_{4}$ , both of rank $6$ . Indeed, in $Q_{15}$ the dual vectors $(1/3,-1/3)$ and $(1/5,1/5)$ have norms $2/3$ and $2/5$ and are orthogonal. Together with the dual of $A_{4}$ , they give the last row’s opposite primary forms after multiplying the $5$ -primary generators by $2$ . The other rows are verified in the same way from their coordinate models. Glue the full discriminant groups along these opposite forms. The graph of the gluing is maximal isotropic, so the resulting lattice is even and self-dual. Its intersection with either rational summand is exactly the prescribed summand lattice. This also preserves the earlier marked $D_{7}$ intersection and all the vectors $t_{y}$ . ∎

Formal reference. SRG266/Completion/Rank24Completion.lean

exists_rank24_completion.

4. The root system is forced

A root means a lattice vector of squared norm $2$ . The first step is to show that the marked $D_{7}$ cannot acquire roots joining it to the other summands.

Lemma 4.1 (Root isolation).

Every root of $\mathcal{L}$ is either a root of the marked $D_{7}$ or is orthogonal to its entire seven-dimensional span.

Proof.

Write a root as $(v,a,w)\in U\perp\mathbb{Q}^{7}\perp W$ . Integrality against $D_{7}$ implies $a\in D_{7}^{*}$ . If $0<\lVert a\rVert^{2}<2$ , the elementary coordinate description of $D_{7}^{*}$ gives either $a=\pm e_{i}$ , of norm $1$ , or seven half-integral coordinates $\pm 1/2$ , of norm $7/4$ . Since $(v,a,w)$ pairs integrally with every $(u_{y},s,0)$ ,

\langle v,u_{y}\rangle+\langle a,s\rangle\in\mathbb{Z}.

In the first case $\langle a,s\rangle\in\mathbb{Z}+1/2$ ; in the second it is an odd multiple of $1/4$ . Thus, with $d=2-\lVert a\rVert^{2}>0$ , every index satisfies

\langle v,u_{y}\rangle^{2}\geq d/4.

On the other hand, the root norm and (9) give

\sum_{y}\langle v,u_{y}\rangle^{2}=45\lVert v\rVert^{2}\leq 45d.

This would imply $220\leq 180$ . Therefore a nonzero $a$ has norm $2$ , and positive definiteness forces $v=w=0$ . The marked intersection in Proposition 3.1 then gives $a\in D_{7}$ . ∎

The next identity is due to Venkov [30]. Together with the ADE second moments, it implies that a nonempty rank- $24$ root system has full rank and a common Coxeter number. We reproduce the argument needed for our marked lattice, rather than invoke the Niemeier classification.

Lemma 4.2 (Venkov’s harmonic root identity).

For the root set $R(\mathcal{L})$ ,

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

(12)

Proof.

For fixed real vectors $v,w$ , the polynomial

p_{v,w}(x)=24\langle x,v\rangle\langle x,w\rangle-\langle v,w\rangle\lVert x\rVert^{2}

is homogeneous and harmonic of degree $2$ . By the harmonic-theta transformation theorem of Hecke and Schoeneberg, its theta series on an even unimodular lattice of rank $24$ is a level-one cusp form of weight $14$ ; see [17, Chapter 3]. The space of such cusp forms is zero: division by the discriminant cusp form identifies it with the space of weight-two modular forms, which is zero [17, Chapter 2]. The coefficient of $q$ in this vanishing theta series is precisely $24\sum_{r}\langle r,v\rangle\langle r,w\rangle-2|R(\mathcal{L})|\langle v,w\rangle$ .

In Lean, the analytic step includes the Gaussian Fourier transform, Poisson summation, convergence of the weighted theta series, and its modular transformation and cusp conditions. Only then is Mathlib’s level-one theory applied, specifically CuspForm.discriminantEquiv and ModularForm.levelOne_weight_two_rank_zero. These belong to Chris Birkbeck’s development of level-one dimension formulas for the sphere-packing formalization [21, Section 2.3]. Our application is in SRG266/Lattice/LevelOneWeight14.lean. The root identity is therefore not a placeholder for a classification theorem. ∎

Proposition 4.3.

The lattice $\mathcal{L}$ has $288$ roots, which span its rational space. Its root system is $A_{11}\perp D_{7}\perp E_{6}$ , with the $D_{7}$ factor equal to the marked factor.

Proof.

For $D_{7}$ , summing over the roots $\pm e_{i}\pm e_{j}$ gives

\sum_{r\in R(D_{7})}\langle r,a\rangle\langle r,b\rangle=24\langle a,b\rangle.

Restrict (12) to the marked span and use Lemma 4.1. It follows that $|R(\mathcal{L})|/12=24$ , so there are $288$ roots. The now positive-definite second moment also shows that the roots span.

An integral norm-two root system is simply laced. Its simple-root graph is a disjoint union of positive-definite ADE diagrams; for the standard root-system classification and Coxeter numbers, see [7, Chapters 4–6]. The second-moment scalar on an irreducible component is twice its Coxeter number, so every component here has Coxeter number $12$ . The only possibilities are $A_{11}$ , $D_{7}$ , and $E_{6}$ . Since the isolated marked $D_{7}$ is a full component, the remaining rank $17$ must be $11+6$ . This gives the stated layout. The root counts $132+84+72=288$ agree with the moment calculation. ∎

Formal reference. SRG266/Completion/RootLayout.lean

exists_rank24_root_layout.

5. First moments, component masses, and the final obstruction

Fix the completion and a root-coordinate isometry supplied by Proposition 4.3. Denote the real spans of $A_{11}$ and $E_{6}$ by $E_{A}$ and $E_{E}$ . The marked identification gives two orthogonal decompositions of the same space:

D_{7}^{\perp}=U\perp W=E_{A}\perp E_{E}.

(13)

For each original index $y$ put $a_{y}=\operatorname{pr}_{E_{A}}t_{y}$ and $e_{y}=\operatorname{pr}_{E_{E}}t_{y}$ . Then $u_{y}=a_{y}+e_{y}$ in this identification, and

\sum_{y}a_{y}=0,\qquad\sum_{y}e_{y}=0,\qquad\lVert a_{y}\rVert^{2}+\lVert e_{y}\rVert^{2}=9/4.

(14)

Integrality against roots places $a_{y}$ in $A_{11}^{*}$ and $e_{y}$ in $E_{6}^{*}$ .

5.1. Two short-vector types

Realize $A_{11}$ as the integer zero-sum lattice on $12$ coordinates. A vector of its dual has coordinates

z_{i}-b/12,\qquad z_{i}\in\mathbb{Z},\qquad\sum_{i}z_{i}=b,

where one may choose $0\leq b\leq 11$ . Its norm is at least $b(12-b)/12$ , with equality exactly when all $z_{i}$ are $0$ or $1$ ; its norm modulo $2\mathbb{Z}$ is $11b^{2}/12$ . The discriminant group of $E_{6}$ is cyclic of order $3$ . The trivial class has even norm; each nontrivial class has minimum $4/3$ and norms congruent to $4/3$ modulo $2\mathbb{Z}$ . Combining these facts with (14) leaves just

\begin{array}[]{c|c|c}b&\lVert a_{y}\rVert^{2}&\lVert e_{y}\rVert^{2}\\ \hline\cr 3\text{ or }9&9/4&0\\ 1\text{ or }11&11/12&4/3.\end{array}

(15)

In each case the $A_{11}$ lower bound is attained, so the integer coordinates are binary. These statements use short-vector inequalities, not a list of vectors in a shell.

There is also a global choice of orientation. If the $E_{6}$ class of index $y$ is denoted by $\epsilon_{y}\in\{0,1,-1\}$ , integrality of (11) gives

12\mid 21-b_{y}b_{z}+16\epsilon_{y}\epsilon_{z}.

(16)

Choose an index with nontrivial $E_{6}$ class, if one exists, and compare all indices with it in this congruence. After possibly reversing all $A_{11}$ coordinates, the two types become

\begin{array}[]{c|c|c|c}\text{type}&b&\lVert a_{y}\rVert^{2}&e_{y}\\ \hline\cr\mathrm{I}&9&9/4&0\\ \mathrm{II}&1&11/12&\lVert e_{y}\rVert^{2}=4/3,\quad e_{y}\in\delta\omega_{E}+E_{6},\end{array}

(17)

for one fixed $\delta\in\{1,-1\}$ and a generator $\omega_{E}$ of the dual quotient. If all classes are trivial, the same congruence forces all labels to be $3$ , or all to be $9$ , and the same normalization applies.

Formal reference. SRG266/Lattice/ShortFrameLabelNormalization.lean

shortFrameLabel_global_orientation.

5.2. The type- $A$ alternative and root placement

We shall prove in Section 6 that the required quasi-symmetric $2$ - $(56,12,9)$ design does not exist. We use that result here only through the following elementary implication.

Lemma 5.1.

The family $(e_{y})$ is not identically zero.

Proof.

If every $e_{y}=0$ , the normalized $A_{11}$ coordinates have binary weight $9$ . Complement their supports to obtain binary columns $w_{y}$ of weight $3$ on $12$ coordinates. Centering subtracts $(1/4)\mathbf{1}$ , and hence

\langle w_{y},w_{z}\rangle=\langle a_{y},a_{z}\rangle+3/4=L_{yz}.

Let $F$ be the resulting $12\times 220$ matrix. Its rank is $12$ , since $F^{\mathsf{T}}F=L$ . The centroid is an integral vector $q$ in these coordinates and $F^{\mathsf{T}}q=15\mathbf{1}$ . Because $F^{\mathsf{T}}(5\mathbf{1})=15\mathbf{1}$ and $F^{\mathsf{T}}$ is injective, we have $q=5\mathbf{1}$ . Thus $F\mathbf{1}=11q=55\mathbf{1}$ . The support of any row is a $55$ -coclique in $H$ : an edge of $H$ has zero Gram entry, whereas two columns sharing a row have positive product. Adjoining $o$ gives a $56$ -coclique in $\Gamma$ .

A coclique $C_{0}$ of this size meets the Hoffman bound. Its equality case [9, Section 3.5] forces every outside vertex to have $12$ neighbours in $C_{0}$ . These neighbourhoods form a $2$ - $(56,12,9)$ design. This is an instance of the regular-set and quasi-symmetric-design correspondence [27, 1]. To obtain its intersections explicitly, write $M_{0}$ for its incidence matrix and $A_{0}$ for the adjacency matrix outside the coclique. The blocks of (1) imply

M_{0}M_{0}^{\mathsf{T}}=36I+9J,\qquad M_{0}A_{0}=9J-9M_{0},\qquad M_{0}^{\mathsf{T}}M_{0}+A_{0}^{2}=36I-9A_{0}+9J.

The symmetric matrix $Z_{0}=M_{0}^{\mathsf{T}}M_{0}-(9I+3J-3A_{0})$ has zero diagonal and satisfies $Z_{0}^{2}=-45Z_{0}$ . Its diagonal square entries are sums of squares, so $Z_{0}=0$ . Distinct design blocks therefore meet in $0$ or $3$ points, contradicting Theorem 6.1. ∎

Formal reference. SRG266/Completion/TypeAFactorization.lean

lorentzian_type_A_binary_factorization.

Each of the four complements in Table 1 contains an $A_{4}$ chain. Connected root chains must lie wholly in one of the two components $A_{11},E_{6}$ : a root is supported in one component, and adjacent roots have nonzero pairing. We next show that an $A_{4}$ chain of the complement cannot lie in $E_{6}$ .

Lemma 5.2.

Suppose an $A_{4}$ root chain lies in $E_{6}$ . Vectors $v,w\in E_{6}^{*}$ of norm $4/3$ in the same nontrivial discriminant class, both orthogonal to this chain, satisfy $\langle v,w\rangle\geq 1/3$ .

Proof.

The pairing is congruent to $4/3$ modulo $\mathbb{Z}$ . Cauchy–Schwarz bounds it below by $-4/3$ , so the only possibility below $1/3$ is $-2/3$ . In that case $v-w$ and $v+2w$ have Gram matrix $\left(\begin{smallmatrix}4&-2\\ -2&4\end{smallmatrix}\right)$ . Together with the orthogonal $A_{4}$ chain these six rational vectors have Gram determinant $5\cdot 12=60$ . Every rational basis of the $E_{6}$ space has determinant $3d^{2}$ for some $d\in\mathbb{Q}$ . This would give $d^{2}=20$ , which is impossible. ∎

If a complementary $A_{4}$ lay in $E_{6}$ , every $e_{y}$ would be orthogonal to it. By the common-coset normalization and Lemma 5.2, all pairings among the nonzero $e_{y}$ would be positive. But their sum is zero by (14). Pairing a nonzero member with that sum is a contradiction. Thus they would all vanish, contrary to Lemma 5.1. Every complementary $A_{4}$ , and consequently every complementary $A_{5}$ , therefore lies in $A_{11}$ .

5.3. Masses from a constant coordinate block

An $A_{4}$ root chain in $A_{11}$ is, up to signed orientation and coordinate permutation, a chain of differences on five of the twelve coordinates. Orthogonality makes these five coordinates equal in every $a_{y}$ . In type I the corresponding five binary entries must all be $1$ , because there are only three zero entries in total; in type II they must all be $0$ , because there is only one entry equal to $1$ . Their common centered coordinates are thus $1/4$ and $-1/12$ . If $n_{0},n_{1}$ count the two types, the first moment yields

n_{0}+n_{1}=220,\qquad n_{0}/4-n_{1}/12=0.

It follows that

n_{0}=55,\quad n_{1}=165,\qquad\sum_{y}\lVert a_{y}\rVert^{2}=275,\qquad\sum_{y}\lVert e_{y}\rVert^{2}=220.

(18)

The argument applies to every complement in the table. It counts indices; no injectivity of the projection maps is used.

Formal reference. SRG266/Lattice/A11FirstMomentCounts.lean

a11_A4_first_moment_counts.

5.4. Trace bounds eliminate three complements

For $v\in E_{A}$ and $w\in E_{E}$ , equation (9) and orthogonal projection give

\sum_{y}\langle v,a_{y}\rangle^{2}\leq 45\lVert v\rVert^{2},\qquad\sum_{y}\langle w,e_{y}\rangle^{2}\leq 45\lVert w\rVert^{2}.

(19)

More generally, if a family in a $d$ -dimensional Euclidean space satisfies this bound and is orthogonal to a $t$ -dimensional subspace, its total squared norm is at most $45(d-t)$ . This follows by summing the bound over an orthonormal basis of the orthogonal complement.

Both $E_{6}$ and $H_{6}$ in Table 1 contain an $A_{5}$ . It must lie in $E_{A}$ , making the $A$ -mass at most $45(11-5)=270$ , contrary to (18). For $C=A_{2}\perp A_{4}$ , the $A_{4}$ again lies in $E_{A}$ . If the $A_{2}$ lies in $E_{E}$ , the $E$ -mass is at most $45(6-2)=180$ . If it lies in $E_{A}$ , the $A$ -mass is at most $45(11-6)=225$ . Both contradict (18). Hence

C=A_{4}\perp Q_{15}.

(20)

5.5. The binary projection trace

Let $r_{1},r_{2}$ be the specified basis of $Q_{15}$ , so $\lVert r_{1}\rVert^{2}=\lVert r_{2}\rVert^{2}=4$ and $\langle r_{1},r_{2}\rangle=1$ . Write $v=\operatorname{pr}_{E_{E}}r_{1}$ and $w=\operatorname{pr}_{E_{E}}r_{2}$ . The $A_{4}$ part of $W$ is contained in $E_{A}$ , so only these two vectors contribute to the projection of $W$ onto $E_{E}$ . The tight frame identity, now used as an exact identity rather than an inequality, gives

	$\displaystyle\sum_{y}\lVert e_{y}\rVert^{2}$	$\displaystyle=45\bigl(6-\operatorname{tr}(\operatorname{pr}_{E_{E}}\operatorname{pr}_{W}\|_{E_{E}})\bigr)$
		$\displaystyle=270-3\bigl(4\lVert v\rVert^{2}+4\lVert w\rVert^{2}-2\langle v,w\rangle\bigr).$		(21)

The factor $1/15$ in the projection trace is the reciprocal of the binary Gram determinant: the inverse matrix is $\frac{1}{15}\left(\begin{smallmatrix}4&-1\\ -1&4\end{smallmatrix}\right)$ . Equating (21) with the $E$ -mass $220$ determines the otherwise unknown projection angle.

Lemma 5.3.

There are integers $x,y,z$ with

x=3\lVert v\rVert^{2},\quad y=3\lVert w\rVert^{2},\quad z=3\langle v,w\rangle,

such that

x,y\in\{0,4,6,12\},\qquad z^{2}\leq xy,\qquad x=y=6\ \Longrightarrow\ 3\mid z.

(22)

Proof.

The $E_{6}$ projections of $r_{i}\in\mathcal{L}$ belong to $E_{6}^{*}$ . Their norms are nonnegative and at most $4$ , and are congruent to either $0$ or $4/3$ modulo $2\mathbb{Z}$ . The only preliminary possibilities are $0,4/3,2,10/3,4$ . A norm $10/3$ would leave an $A_{11}^{*}$ projection of norm $2/3$ , smaller than its least positive norm $11/12$ . Thus it is excluded. Three times any pairing in $E_{6}^{*}$ is integral, and Cauchy–Schwarz gives the displayed inequality. Finally an $E_{6}^{*}$ vector of norm $2$ lies in $E_{6}$ itself, so two such vectors have an integral pairing; in the scaled notation $3\mid z$ . ∎

Proof of Theorem 1.1.

Apply the preceding constructions to the hypothetical graph. The type- $A$ alternative is excluded by Theorem 6.1. The trace bounds leave (20), and (21) becomes

4x+4y-2z=50.

(23)

Equivalently $z=2x+2y-25$ . Using $z^{2}\leq xy$ , the only pair from the four allowed values, up to interchanging $x,y$ , is $x=y=6$ . For clarity the values of $z^{2}-xy$ for the ten unordered pairs are

\begin{array}[]{c|rrrrr}(x,y)&(0,0)&(0,4)&(0,6)&(0,12)&(4,4)\\ z^{2}-xy&625&289&169&1&65\\ \hline\cr(x,y)&(4,6)&(4,12)&(6,6)&(6,12)&(12,12)\\ z^{2}-xy&1&1&-35&49&385\end{array}

For $x=y=6$ , equation (23) gives $z=-1$ , contradicting $3\mid z$ . This completes the contradiction. ∎

Formal reference. SRG266/Completion/MomentBounds.lean

no_q15_projection_trace.

The last arithmetic check has only four possible values per norm. It is not a substitute encoding of the removed shell searches: its inputs are the projection norms of two specified complementary vectors, obtained from the actual marked completion and its frame trace.

6. The design obstruction without classification

This section is independent of the rank- $24$ construction. Its input is only a hypothetical quasi-symmetric design with the indicated parameters.

Theorem 6.1 (Munemasa–Tonchev, with an internal alternative proof).

There is no quasi-symmetric $2$ - $(56,12,9)$ design with block intersection numbers $0$ and $3$ .

The statement is due to Munemasa and Tonchev [25]. We give the argument used to prove it inside the formalization. The central point is that local triangular reconstructions can be made compatible across all $56$ choices of a deleted point. The resulting canonical biplane extends the hypothetical design by one point. A local graph obstruction then replaces the biplane and code classifications.

6.1. Local triangular graphs

Let $\mathcal{D}$ be the hypothetical design on a point set $P_{0}$ . It has $210$ blocks and replication number $45$ . Fix $p\in P_{0}$ . The $45$ blocks through $p$ , with $p$ deleted, have size $11$ , pairwise intersection $2$ , and replication $9$ on the remaining $55$ points. Their dual is a $2$ - $(45,9,2)$ design. For $q,r\neq p$ let $m_{p}(q,r)$ count blocks through $p,q,r$ ; set $m_{p}(q,q)=9$ . Double counting gives

\sum_{r\neq p,q}m_{p}(q,r)=90,\qquad\sum_{r\neq p,q}m_{p}(q,r)^{2}=162.

Since $(t-1)(t-2)\geq 0$ for every nonnegative integer $t$ , the sum of these expressions over $54$ points is $162-3\cdot 90+2\cdot 54=0$ . Every off-diagonal multiplicity is therefore $1$ or $2$ .

Join $q,r$ when $m_{p}(q,r)=1$ . There are $18$ neighbours of each vertex, and the mixed moment

\sum_{s\neq p}m_{p}(q,s)m_{p}(r,s)=162+9m_{p}(q,r)

gives $14-5m_{p}(q,r)$ common neighbours. The link graph thus has parameters $(55,18,9,4)$ . It is the triangular graph $T(11)$ . The needed uniqueness result [14] is proved internally: its neighbourhoods split into two $9$ -cliques with a matching between them; the resulting grand $10$ -cliques number $11$ , each vertex belongs to two, and pairs of grand cliques meet in one vertex. Assigning to a vertex its two grand cliques gives the required edge coordinates. Choose an identification

\eta_{p}:P_{0}\setminus\{p\}\longrightarrow\binom{[11]}{2}.

For distinct $p,q,r$ it satisfies

\kappa(p,q,r):=\#\{B\in\mathcal{D}:p,q,r\in B\}=2-|\eta_{p}(q)\cap\eta_{p}(r)|.

(24)

The left side is symmetric in the three points, providing compatibility between the different choices of local coordinates.

6.2. Ternary self-orthogonality glues the stars

For $a\in[11]$ define the closed star

S_{p,a}=\{p\}\cup\{q\neq p:a\in\eta_{p}(q)\}.

It has $11$ points. Let $\mathcal{C}\subseteq\mathbb{F}_{3}^{P_{0}}$ be the code spanned by the incidence vectors of the original blocks. Because both block size and all block intersections are divisible by $3$ ,

\mathcal{C}\subseteq\mathcal{C}^{\perp}.

(25)

The following observation uses this code without enumerating its words.

Lemma 6.2.

Every complemented star $\mathbf{1}-\mathbf{1}_{S_{p,a}}$ lies in $\mathcal{C}$ . The closed stars, after duplicates are identified, are the blocks of a canonical $2$ - $(56,11,2)$ biplane $\mathcal{B}$ . They satisfy

	$\displaystyle\|B\cap S\|$	$\displaystyle\in\{0,3\}\quad(B\in\mathcal{D},\ S\in\mathcal{B}),$		(26)
	$\displaystyle\kappa(p,q,r)+\#\{S\in\mathcal{B}:p,q,r\in S\}$	$\displaystyle=2\quad(p,q,r\text{ distinct}).$		(27)

Proof.

For $q\neq p$ take the sum in $\mathbb{F}_{3}^{P_{0}}$ of the original block vectors containing $p,q$ . Its coordinate at $x$ is $\kappa(p,q,x)$ , with value $9=0$ at $x=p,q$ . If $\eta_{p}(q)=\{a,b\}$ , equation (24) writes this word as $2j_{p}-s_{p,a}-s_{p,b}$ , where $j_{p}$ is $1$ outside $p$ and $s_{p,a}$ is the open-star vector. Combining the three words for $\{a,b\},\{a,c\},\{b,c\}$ gives $j_{p}-s_{p,a}$ in the code. This is the complemented closed-star vector. Self-orthogonality now implies

|S_{p,a}\cap S_{q,b}|\equiv 2\pmod{3}.

(28)

We detail why a closed star can be re-rooted at any one of its points; this prevents treating unrelated local biplanes as a single object. Let $S=S_{p,a}$ and $q\in S\setminus\{p\}$ . In the $q$ -coordinates, the ten edges representing $S\setminus\{q\}$ , including the central edge itself, all meet the central edge representing $p$ . By (28), every coordinate degree of this ten-edge set is $1$ modulo $3$ . A vertex outside the central edge has degree at most $2$ , hence degree exactly $1$ . Thus two noncentral edges meet precisely when they attach to the same end of the central edge. For triples on $S\setminus\{p\}$ this gives the two-colour link parity identity. On four distinct points, write $A,B,C,D$ for the assertions that each of its four triples has multiplicity $1$ . The three link identities are $A\leftrightarrow(B\leftrightarrow C)$ , $A\leftrightarrow(B\leftrightarrow D)$ , and $A\leftrightarrow(C\leftrightarrow D)$ ; together they force $A$ . Using a fourth point of $S\setminus\{p\}$ proves that every triple in $S$ has multiplicity $1$ . Consequently, in coordinates at any $q\in S$ , all ten edges are pairwise intersecting. More than three pairwise intersecting edges of a complete graph form a star. Hence $S=S_{q,b}$ for some $b$ .

Two closed stars have nonempty intersection by (28). Re-rooting at a common point shows that distinct ones meet in exactly two points. At each point there are exactly $11$ stars, and each pair of points lies in two. Counting point–star incidences gives $56$ distinct stars. These are the stated biplane.

For a block $B$ containing $p$ , its $11$ edges in the $p$ -coordinates have degree $2$ at each of the $11$ coordinates. This follows from the local incidence moments (and is proved before any star is glued). If $B\cap S$ is nonempty, re-root at $p\in B\cap S$ ; the intersection then consists of $p$ and the two edges at the star centre, giving $3$ . Finally the number of biplane blocks containing $p,q,r$ is $|\eta_{p}(q)\cap\eta_{p}(r)|$ , so (27) follows from (24). ∎

Formal reference. SRG266/Design/CanonicalBiplane.lean

canonicalBiplane_triple_complement.

Adjoin a new point $\infty$ and extend the $56$ biplane blocks by it, retaining the $210$ original blocks. Equations (26)–(27) give a $3$ - $(57,12,2)$ design $\mathcal{T}$ with $266$ blocks and block intersections $0,3$ . Triples involving $\infty$ use the biplane pair equation; the others use (27). Its replication number is $56$ and its pair multiplicity is $11$ . This is a construction from $\mathcal{D}$ , not an appeal to a classification of all biplanes or of their ternary codes.

6.3. The associated Krein graph

We use the classical point–block construction for triangle-free strongly regular graphs; see [12, Chapter 5] and the proof of the Krein-graph characterization in [13]. Construct a graph $K$ on the disjoint union of one new vertex $*$ , the $57$ points of $\mathcal{T}$ , and its $266$ blocks. Join $*$ to all points, join a point to its incident blocks, and join two blocks when they are disjoint. There are no other edges. If $M_{1}$ is the incidence matrix and $A_{\mathrm{disj}}$ is the block disjointness matrix, then

	$\displaystyle M_{1}M_{1}^{\mathsf{T}}$	$\displaystyle=45I+11J,\qquad M_{1}^{\mathsf{T}}M_{1}=9I+3J-3A_{\mathrm{disj}},$
	$\displaystyle M_{1}A_{\mathrm{disj}}$	$\displaystyle=12(J-M_{1}).$

These equations give, for the adjacency matrix $A_{K}$ ,

A_{K}^{2}=45I-12A_{K}+12J.

(29)

Thus $K$ is an $\operatorname{SRG}(324,57,0,12)$ . The triple-design equation further gives

|\Gamma_{K}(a)\cap\Gamma_{K}(b)\cap\Gamma_{K}(c)|=3\quad\text{for every independent triple }\{a,b,c\}.

(30)

For example, if all three vertices are points the common neighbours are $*$ and their two incident triple blocks. The other vertex types follow by expanding products of incidence entries and using the same triple equation; these expansions are formalized in SRG266/Design/Krein/TripleMoments.lean.

We now use only the local identities available for this constructed graph. For an independent triple $\tau$ , put $\tau^{\circ}=\bigcap_{v\in\tau}\Gamma_{K}(v)$ . Then $\tau^{\circ}$ is an independent triple and $(\tau^{\circ})^{\circ}=\tau$ . The six vertices $\Delta=\tau\cup\tau^{\circ}$ induce $K_{3,3}$ . Every vertex outside $\Delta$ has $0$ , $1$ , or $2$ neighbours in it: it cannot meet both sides without a triangle, and meeting all three vertices of one side would put it in the other side. Partition these outside vertices into $X_{0},X_{1},X_{2}$ by this number.

Lemma 6.3 (The cubic pair).

One has $|X_{0}|=48$ , $|X_{1}|=216$ , and $|X_{2}|=54$ . The induced graphs on $U_{0}=\Delta\cup X_{0}$ and $U_{2}=X_{2}$ are cubic graphs on $54$ vertices. Each vertex has $18$ neighbours in the other set. If $A_{0},A_{2}$ are their adjacency matrices and $B$ is the cross-incidence matrix, then

BB^{\mathsf{T}}=(A_{0}-3I)^{2}+6J,\qquad B^{\mathsf{T}}B=(A_{2}-3I)^{2}+6J.

(31)

Proof.

Counting vertices, edges to $\Delta$ , and common-neighbour pairs in $\Delta$ gives

|X_{0}|+|X_{1}|+|X_{2}|=318,\quad|X_{1}|+2|X_{2}|=324,\quad|X_{2}|=54.

For the last count there are six nonadjacent pairs in $\Delta$ , each with $12$ common neighbours, of which three are inside $\Delta$ . The stated sizes follow. The analogous counts with one vertex fixed, using (30), give the local degrees $3$ and $18$ . For distinct nonadjacent $x,y\in U_{i}$ , they also give

|\Gamma(x)\cap\Gamma(y)\cap U_{2-i}|=6+|\Gamma(x)\cap\Gamma(y)\cap U_{i}|.

For adjacent vertices both common-neighbour counts vanish; on the diagonal they are $18$ and $3$ . These three cases are exactly (31). ∎

Taking traces of the squares in (31) gives $\operatorname{tr}A_{0}^{4}=\operatorname{tr}A_{2}^{4}$ . Indeed the two Gram products have equal square traces, while both cubic graphs have $54$ vertices, trace zero, second trace $162$ , and third trace zero. A cubic graph on $n$ vertices without four-cycles has fourth trace $15n$ . The graph on $U_{0}$ contains $\Delta=K_{3,3}$ , so its fourth trace is strictly greater than $15\cdot 54$ . The graph on $X_{2}$ must therefore contain a four-cycle.

Lemma 6.4 (Unique companion).

There is exactly one induced $K_{3,3}$ whose vertices lie in $X_{2}$ . Together with $\Delta$ it induces $K_{6,6}$ minus a perfect matching.

Proof.

We first record the two local counting obstructions that make the four-cycle sufficient. For opposite vertices $x,y$ of a four-cycle in $X_{2}$ , let $\nu_{xy}=|\Gamma(x)\cap\Gamma(y)\cap X_{2}|$ and $d_{xy}=|\Gamma(x)\cap\Gamma(y)\cap\Delta|$ . Then $2\leq\nu_{xy}\leq 3$ and $d_{xy}\geq 1$ . For $Z_{xy}=(\Gamma(x)\cup\Gamma(y))\cap X_{0}$ , the local counts give

|Z_{xy}|=26+d_{xy}-\nu_{xy}.

(32)

If $f,g$ are the other opposite vertices, triangle-freeness makes $Z_{xy}$ and $Z_{fg}$ disjoint. If $\nu_{xy}=2$ , their sizes would be at least $25$ and $24$ , contradicting $|X_{0}|=48$ . Thus every pair in $X_{2}$ with at least two common neighbours there has three. Cubicity now completes the four-cycle to a $K_{3,3}$ component of the graph on $X_{2}$ .

Second, there is no $K_{3,3}$ inside $X_{0}$ . For nonadjacent distinct $x,y\in X_{0}$ , the local common counts give

|\Gamma(x)\cap\Gamma(y)\cap X_{1}|+2|\Gamma(x)\cap\Gamma(y)\cap X_{0}|=6.

If the second common-neighbour count were three, the first would vanish. All common neighbours would then have an even number of neighbours in $\tau$ (zero or two). But summing their degrees into $\tau$ counts, for each $s\in\tau$ , the three common neighbours of the independent triple $x,y,s$ , and so gives the odd number $9$ . This contradiction bounds common-neighbour counts inside $X_{0}$ by $2$ and excludes a $K_{3,3}$ there.

Two distinct $K_{3,3}$ components inside $X_{2}$ would be disjoint and have no edges between them. Relative to either biclique, the other would lie in its zero-neighbour class, contradicting the preceding obstruction. This proves uniqueness. Every vertex of the companion has two neighbours in $\Delta$ . Counting the $12$ cross edges and using the outside-degree bound shows that every vertex of $\Delta$ also has two neighbours in the companion. Triangle-freeness makes the two bipartitions compatible. After choosing their orientations, the union has two independent sides of size $6$ , and every vertex meets five vertices on the other side. The missing edges are consequently a perfect matching. ∎

Formal reference. SRG266/Design/Krein/Companion.lean

exists_unique_biclique_companion.

Call an induced $K_{6,6}$ minus a perfect matching a crown. Every independent triple lies in the crown constructed above, and this crown is unique. To see uniqueness, an independent triple in any crown lies in one side: a vertex on one side has only one non-neighbour on the other, so an independent triple cannot meet both sides. Its three common neighbours are the opposite side minus the three matched vertices. The remaining six vertices form a biclique in its class $X_{2}$ , hence must be its unique companion.

6.4. Steiner completion and divisibility

Choose distinct nonadjacent vertices $a,b$ of $K$ and let $\Omega=\Gamma_{K}(a)\cap\Gamma_{K}(b)$ . This is an independent set of size $12$ . For each crown $\mathcal{W}$ meeting $\Omega$ in four vertices, take $\mathcal{W}\cap\Omega$ as a block, identifying repeated subsets. Every triple $\tau\subset\Omega$ lies in its unique crown $\mathcal{W}$ . In a bipartition of $\mathcal{W}$ , say $\tau$ lies on the left, its common neighbours are exactly the three unmatched vertices on the right. Both $a,b$ belong to this triple of common neighbours. Their common neighbours in the crown are the four vertices on the left other than their two distinct matching partners. Hence $|\mathcal{W}\cap\Omega|=4$ . Any other block containing $\tau$ would come from another crown containing the same independent triple, which is impossible. We have constructed a Steiner $3$ - $(12,4,1)$ design.

Fix a point in such a design. The $\binom{11}{2}=55$ triples containing that point must be partitioned into the $\binom{3}{2}=3$ triples contributed by each block through it. Its integral replication number $r$ would satisfy $3r=55$ . This contradiction proves Theorem 6.1.

Formal reference. SRG266/Design/Krein/SteinerCompletion.lean

no_quasi_symmetric_design.

The intervening $3$ - $(57,12,2)$ design was already excluded by Kaski and Östergård [22, Corollary 2], combining their classification with the nonextendability computations of Key and Tonchev [23]. Bagchi’s earlier claimed proof [3], with its subsequent corrigendum, contained a linear-algebra error; Key and Tonchev discuss the error and credit Brouwer with finding it. We do not use that argument. The general nonexistence of the Krein graph with parameters $(324,57,0,12)$ was proved by Gavrilyuk and Makhnev [19]. The purpose of these constructions is to close the required dependency inside Lean with local moment, parity, and divisibility arguments.

7. Formal verification and reproducibility

7.1. Statement and trusted boundary

The development uses Lean 4 [16] and Mathlib [29]. The public theorem in Main.lean is

theorem SRG266.nonexistence
{V : Type u} [Fintype V] (G : SimpleGraph V)
[DecidableRel G.Adj] :
$\neg$ G.IsSRGWith 266 45 0 9

Here IsSRGWith is Mathlib’s own definition, not a weakened project-specific substitute. The type $V$ is arbitrary and universe polymorphic. The finite-type and decidable-adjacency instances support finite counting; no graph-theoretic hypothesis is hidden in a typeclass.

The axiom collector for the final theorem reports exactly

\text{{propext}},\qquad\text{{Classical.choice}},\qquad\text{{Quot.sound}}.

There are no added mathematical axioms, assumed host lists, unproved design obstructions, or external solver answers in this dependency closure. Tactics construct proof terms checked by the kernel. The source audit rejects proof holes and the prohibited external-evaluation mechanisms, and checks that all $258$ project proof modules are reachable from Main.lean. The axiom check also elaborates the public statement again as an example, so it checks the theorem’s type as well as its axioms.

We use certificate-free in the following specific sense: the build does not consume external Hall, Farkas, SAT/LRAT, shell-enumeration, or similar infeasibility certificates. Small finite arithmetic arguments remain, for example the four norm values in Lemma 5.3 and the primary discriminant normal forms. Naturally the Lean proof term itself is a certificate in the general proof-theoretic sense. We do not claim that finite case distinctions have disappeared.

Kernel checking establishes the formal theorem under the displayed axioms. It does not independently certify the accuracy of every sentence in this paper, the historical attribution, or the absence of hardware and implementation faults. These are separate responsibilities.

7.2. Archived source and build procedure

Release v2.0.0 of the formalization is archived at DOI 10.5281/zenodo.22509839 [2]. Its Git commit is

5fb00e6db138d6df962d71b3b2e1a26ac42a9e59.

The archive contains the proof source; it is not an archive of this manuscript. The Lean toolchain is pinned to leanprover/lean4:v4.33.1. Mathlib is pinned to the following commit, corresponding to its tag v4.33.1:

0df444a360eaa60ab8c11dca51a86af692955474.

After installing elan and obtaining that release, a bounded local build can be run as follows:

export LEAN_NUM_THREADS=8
lake exe cache get
python3 scripts/audit.py
lake build
lake env lean scripts/check_axioms.lean

During lake build, the repository passes -j1 and -M4096 to project elaboration subprocesses. Limiting a subprocess to one thread is not by itself a limit on the number of simultaneous Lake jobs; the LEAN_NUM_THREADS environment variable must also be set. The continuous-integration workflow has one verification job, with a thread budget of $2$ , and performs the cache retrieval, source audit, build, and axiom check. It does not distribute project object files between jobs.

For a Linux system supporting user-systemd memory control, the measured eight-core, $32$ -GiB-budget build used the following form of command, after the Mathlib cache had been obtained:

lake clean srg266
systemd-run --user --quiet --wait --pipe \
  --property=MemoryMax=32G --property=MemorySwapMax=0 \
  --working-directory="$PWD" \
  /usr/bin/taskset -c 0-7 /usr/bin/env LEAN_NUM_THREADS=8 \
  python3 scripts/measure.py .lake/measured-build lake build

The CPU numbers should be adjusted to the machine’s topology and allowed CPU set. In the reported run, CPUs $0$ – $7$ represented eight distinct physical cores. Affinity enforced the CPU bound and cgroup memory control enforced the memory bound; a declared quota without an active controller is not evidence of enforcement.

Table 3. Local verification measurements, 6 September 2026. Project object files were cleaned for the Lean build; the Mathlib cache was already present. The nanoda measurement excludes the preceding export.

	Lean project build	nanoda check
Wall time	$884.17$ s ( $14$ min $44$ s)	$24.47$ s
Largest child-process RSS	$3.85$ GiB	$1.81$ GiB
Cgroup peak memory	$3.68$ GiB	$1.81$ GiB
CPU affinity	CPUs $0$ – $7$	CPUs $0$ – $7$
Memory / swap limits	$32$ GiB / $0$	$32$ GiB / $0$
OOM events	$0$	$0$

The machine was an Intel Core i9-10900KF desktop with $64$ GB installed RAM, running Linux 6.8.0-138. The limit was a build budget, not the observed requirement. Maximum child RSS is a per-process high-water mark, not aggregate memory; cgroup accounting is a different measurement and the two values need not coincide. Cache download time and a rebuild of Mathlib from source are not included. Source hashes were recorded and checked unchanged by the measurement script; the proof sources of the archived release agree with this measured source set.

7.3. Independent checking

We exported the dependency closure of SRG266.nonexistence with lean4export and checked it with the independent checker nanoda [24, 26]. The check accepted $77{,}402$ declarations with only the same three permitted axioms and with unsafe axiom allowances disabled. The configuration scripts/nanoda.json enables nat_extension and string_extension, so the check uses nanoda’s implementations of the Nat and String literal extensions supported by the Lean kernel. These extensions belong to the checker’s trusted implementation, rather than adding declared axioms. The pinned revisions used were

lean4export	411dce7db58a3afc60ecab2d211acd1042b593dc
nanoda	05055695879dfebb6628a67da88ceca6cd6b0421.

The exporter’s toolchain pin was adjusted to Lean 4.33.1 before building it. Its export format and the selected nanoda revision were checked for compatibility. With those executables built, the check takes the form

LEAN_NUM_THREADS=1 lake env /path/to/lean4export \
  Main -- SRG266.nonexistence > .lake/nonexistence.ndjson
/path/to/nanoda_bin scripts/nanoda.json \
  < .lake/nonexistence.ndjson

The exported stream had SHA-256

17b9cf9e04de998981a10d1d0a11f854b7b0aebbf3b9a5d59bcf07933d0a94ce.

This is a reproducibility fingerprint of the measured export, not an additional mathematical assumption. Independent checking reduces reliance on a single kernel implementation; it does not certify the exporter, checker, and hardware as infallible.

8. Use of large language models

This project is human-directed and LLM-led in mathematical research and formalization. Kay Akiyama selected the problem and supplied the objective and continuing instructions, and is the author and maintainer responsible for the work. The models were used for strategy, mathematical exploration, formal proof construction, debugging, verification support, and exposition, not merely language polishing.

The release disclosure attributes the initial mathematical research to GPT-5.6 Sol and Claude Fable 5, and the initial Lean formalization to Claude Opus 5 with Claude Code and GPT-5.6 Sol with Codex. GPT-6 Astra carried out the proof-chain contraction and the formalization work that eliminated the large external certificates. This included the certificate-free lattice and design arguments described above. GPT-5.6 Sol assisted with manuscript preparation and review. GPT-6 Astra prepared the present exposition using the formal source and primary literature.

These are workflow-level attributions, not a verified line-by-line allocation of individual lemmas to particular models. No LLM is listed as an author. The correctness claim for the formal theorem rests on proof checking, not on a model’s account of its reasoning. The author remains responsible for the exposition, citations, disclosure, and submission.

9. Conclusion

The obstruction is obtained by preserving a local frame while changing its ambient geometry. The integral centroid provides the arithmetic needed for a marked even unimodular completion. A root-isolation gap and a vanishing harmonic theta series determine its root system. The first moment fixes the two shell-type counts, while the second moment bounds or determines the remaining projections. The terminal contradiction concerns two vectors, rather than a large enumerated shell. The design branch follows the same principle: compatibility across local structures replaces separate searches, and a forced completion ends in an elementary divisibility obstruction.

The result is an end-to-end proof of the nonexistence theorem with no external infeasibility data. The analytic and structural steps enlarge the mathematics developed inside Lean, but remove the dependence on large problem-specific certificates.

Appendix A A map from the argument to the formal source

All paths below are relative to the archived repository. This is a map of the principal interfaces, not a claim that each step occupies only the displayed file. The general-purpose lattice infrastructure is in SRG266/Lattice/; the application-specific assembly is in SRG266/Completion/.

Mathematical step	Formal entry point
Local matrix algebra	SRG266/LocalAlgebra.lean, SRG266/LocalSpectrum.lean
Integral centroid	SRG266/KernelReduction.lean, exists_integral_centroid
Lorentzian change and frame	SRG266/Completion/Lift.lean, SRG266/Completion/Perpendicular.lean
Rank-six complement and marked completion	SRG266/Lattice/RankSixComplements.lean, SRG266/Completion/Rank24Completion.lean
$D_{7}$ isolation	SRG266/Lattice/D7FrameIsolation.lean, d7_root_separation_of_frame
Harmonic theta and roots	SRG266/Lattice/Rank24HarmonicThetaAnalytic.lean, SRG266/Lattice/LevelOneWeight14.lean, SRG266/Completion/RootMoment.lean
Internal ADE analysis	SRG266/Lattice/ADEConnectedClassification.lean, SRG266/Completion/RootLayout.lean
Orientation and first moments	SRG266/Lattice/ShortFrameLabelNormalization.lean, SRG266/Lattice/A11FirstMomentCounts.lean
Complement placement and masses	SRG266/Completion/ResidualRootChain.lean, SRG266/Completion/FrameMassConstruction.lean, SRG266/Completion/Order75FrameMass.lean
Trace exclusions	SRG266/Completion/A5TraceObstruction.lean, SRG266/Completion/A2A4TraceObstruction.lean
Binary endpoint	SRG266/Completion/Q15ProjectionData.lean, SRG266/Completion/Q15TraceObstruction.lean
Binary factorization and coclique	SRG266/Completion/TypeAFactorization.lean, SRG266/NotOneIntegrable.lean, SRG266/CocliqueDesign.lean
Triangular reconstruction	SRG266/Design/TriangularUniqueness.lean
Canonical biplane and extension	SRG266/Design/CanonicalBiplaneCode.lean, SRG266/Design/ClosedStarGluing.lean, SRG266/Design/OnePointExtension57.lean
Krein graph and triple moments	SRG266/Design/Krein/Construction.lean, SRG266/Design/Krein/TripleMoments.lean
Cubic traces and companion	SRG266/Design/Krein/CubicGram.lean, SRG266/Design/Krein/FourthTrace.lean, SRG266/Design/Krein/Companion.lean
Steiner obstruction	SRG266/Design/Krein/SteinerCompletion.lean, no_quasi_symmetric_design
Final statement	Main.lean, SRG266.nonexistence

References

[1] Mohammad Adm, Ryan Bergen, Ferdinand Ihringer, Sam Jaques, Karen Meagher, Alison Purdy, and Boting Yang, Ovoids of generalized quadrangles of order $(q,q^{2}-q)$ and Delsarte cocliques in related strongly regular graphs, Journal of Combinatorial Designs 26 (2018), no. 5, 249–263.
[2] Kay Akiyama, There is no strongly regular graph with parameters $(266,45,0,9)$ , Zenodo, software release v2.0.0, 2026, https://doi.org/10.5281/zenodo.22509839. Source: https://github.com/kay-akiyama/srg266-nonexistence-lean/tree/v2.0.0.
[3] Bhaskar Bagchi, No extendable biplane of order nine, Journal of Combinatorial Theory, Series A 49 (1988), no. 1, 1–12, Corrigendum, ibid. 57 (1991), 162.
[4] Norman L. Biggs, Strongly regular graphs with no triangles, arXiv:0911.2160, 2009, https://arxiv.org/abs/0911.2160.
[5] A. V. Bondarenko, A. Prymak, and D. Radchenko, Non-existence of $(76,30,8,14)$ strongly regular graph, Linear Algebra and its Applications 527 (2017), 53–72.
[6] Andriy Bondarenko, Anton Mellit, Andriy Prymak, Danylo Radchenko, and Maryna Viazovska, There is no strongly regular graph with parameters $(460,153,32,60)$ , Contemporary Computational Mathematics—A Celebration of the 80th Birthday of Ian Sloan (Josef Dick, Frances Y. Kuo, and Henryk Woźniakowski, eds.), Springer, 2018, pp. 131–134.
[7] Nicolas Bourbaki, Lie groups and Lie algebras: Chapters 4–6, Elements of Mathematics, Springer, 2002.
[8] Andries E. Brouwer, Parameters of strongly regular graphs, Online parameter tables, https://aeb.win.tue.nl/graphs/srg/srgtab.html. Accessed 8 September 2026.
[9] Andries E. Brouwer and Willem H. Haemers, Spectra of graphs, Universitext, Springer, 2012.
[10] Andries E. Brouwer and Hendrik Van Maldeghem, Strongly regular graphs, Encyclopedia of Mathematics and its Applications, vol. 182, Cambridge University Press, 2022.
[11] P. J. Cameron, J. M. Goethals, and J. J. Seidel, Strongly regular graphs having strongly regular subconstituents, Journal of Algebra 55 (1978), no. 2, 257–280.
[12] P. J. Cameron and J. H. van Lint, Graphs, codes and designs, London Mathematical Society Lecture Note Series, vol. 43, Cambridge University Press, 1980.
[13] Mingzhu Chen, A. A. Makhnev, and M. S. Nirova, On graphs in which the neighborhoods of vertices are edge-regular graphs without 3-claws, Trudy Instituta Matematiki i Mekhaniki UrO RAN 29 (2023), no. 4, 279–282, In Russian; English translation in Proceedings of the Steklov Institute of Mathematics 323 (2023), suppl. 1, S53–S55.
[14] William S. Connor, The uniqueness of the triangular association scheme, The Annals of Mathematical Statistics 29 (1958), no. 1, 262–266.
[15] John H. Conway and Neil J. A. Sloane, Sphere packings, lattices and groups, third ed., Grundlehren der mathematischen Wissenschaften, vol. 290, Springer, 1999.
[16] Leonardo de Moura and Sebastian Ullrich, The Lean 4 theorem prover and programming language, Automated Deduction—CADE 28, Lecture Notes in Computer Science, vol. 12699, Springer, 2021, pp. 625–635.
[17] Wolfgang Ebeling, Lattices and codes: A course partially based on lectures by Friedrich Hirzebruch, third ed., Advanced Lectures in Mathematics, Springer Spektrum, 2013.
[18] Nick C. Fiala and Willem H. Haemers, 5-chromatic strongly regular graphs, Discrete Mathematics 306 (2006), no. 23, 3083–3096.
[19] A. L. Gavrilyuk and A. A. Makhnev, On Krein graphs without triangles, Doklady Mathematics 72 (2005), no. 1, 591–594, Russian original: Doklady Akademii Nauk 403 (2005), no. 6, 727–730.
[20] Marshall Hall, Jr. and William S. Connor, An embedding theorem for balanced incomplete block designs, Canadian Journal of Mathematics 6 (1954), 35–41.
[21] Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, and Maryna Viazovska, Progress in formalizing sphere packing in dimension 8, arXiv:2604.23468v3, 2026, https://arxiv.org/abs/2604.23468v3.
[22] Petteri Kaski and Patric R. J. Östergård, There are exactly five biplanes with $k=11$ , Journal of Combinatorial Designs 16 (2008), no. 2, 117–127.
[23] J. D. Key and Vladimir D. Tonchev, Computational results for the known biplanes of order 9, Geometry, Combinatorial Designs and Related Structures (J. W. P. Hirschfeld, S. S. Magliveras, and M. J. de Resmini, eds.), London Mathematical Society Lecture Note Series, vol. 245, Cambridge University Press, 1997, pp. 113–122.
[24] Lean contributors, lean4export, Software repository, 2026, https://github.com/leanprover/lean4export. Revision used is recorded in Section 7.
[25] Akihiro Munemasa and Vladimir D. Tonchev, Ternary codes, biplanes, and the nonexistence of some quasisymmetric and quasi-3 designs, Journal of Combinatorial Designs 28 (2020), no. 10, 745–752.
[26] nanoda contributors, nanoda, Independent proof checker, software repository, 2026, https://github.com/ammkrn/nanoda_lib. Revision used is recorded in Section 7.
[27] Arnold Neumaier, Regular sets and quasi-symmetric 2-designs, Combinatorial Theory (Dieter Jungnickel and Klaus Vedder, eds.), Lecture Notes in Mathematics, vol. 969, Springer, 1982, pp. 258–275.
[28] V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, Mathematics of the USSR-Izvestiya 14 (1980), no. 1, 103–167.
[29] The mathlib Community, The Lean mathematical library, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, 2020, pp. 367–381.
[30] B. B. Venkov, Even unimodular 24-dimensional lattices, Sphere Packings, Lattices and Groups (John H. Conway and Neil J. A. Sloane, eds.), Grundlehren der mathematischen Wissenschaften, vol. 290, Springer, third ed., 1999, pp. 429–440.

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

Abstract.

Key words and phrases:

2020 Mathematics Subject Classification

1. Introduction

Theorem 1.1.

Remark 1.2.

The mathematical mechanism

Prior results and scope

2. The local Gram lattice

Lemma 2.1.

Proof.

Lemma 2.2.

Proof.

Proposition 2.3 (Integral centroid).

Proof.

3. A marked completion in dimension twenty-four

3.1. The Lorentzian form and the tight frame

3.2. The marked D7D_{7}

Proposition 3.1 (Marked completion).

Proof of Proposition 3.1.

4. The root system is forced

Lemma 4.1 (Root isolation).

Proof.

Lemma 4.2 (Venkov’s harmonic root identity).

Proof.

Proposition 4.3.

Proof.

5. First moments, component masses, and the final obstruction

5.1. Two short-vector types

5.2. The type-AA alternative and root placement

Lemma 5.1.

Proof.

Lemma 5.2.

Proof.

5.3. Masses from a constant coordinate block

5.4. Trace bounds eliminate three complements

5.5. The binary projection trace

Lemma 5.3.

Proof.

Proof of Theorem 1.1.

6. The design obstruction without classification

Theorem 6.1 (Munemasa–Tonchev, with an internal alternative proof).

6.1. Local triangular graphs

6.2. Ternary self-orthogonality glues the stars

Lemma 6.2.

Proof.

6.3. The associated Krein graph

Lemma 6.3 (The cubic pair).

Proof.

Lemma 6.4 (Unique companion).

Proof.

6.4. Steiner completion and divisibility

7. Formal verification and reproducibility

7.1. Statement and trusted boundary

7.2. Archived source and build procedure

7.3. Independent checking

8. Use of large language models

9. Conclusion

Appendix A A map from the argument to the formal source

References

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

3.2. The marked $D_{7}$

5.2. The type- $A$ alternative and root placement