AI 中文总结
用 Lean 4 无证书证明不存在参数为 (266,45,0,9) 的强正则图，通过格论、theta 恒等式和设计论归谬完成。
AI 中文摘要
我们证明了不存在参数为 $(266, 45, 0, 9)$ 的强正则图。该证明在 Lean 4 和 Mathlib 中形式化，不依赖外部不可行性证书或假定的分类定理。一个假设的图给出一个秩为 $12$ 的整格，具有积分质心。通过洛伦兹型变换、标记的 $D_7$ 粘合以及一个显式的秩六补格，得到一个秩为 $24$ 的正定偶幺模格，连同原始的 $220$ 个向量的索引族。调和 theta 恒等式和根隔离不等式迫使根系为 $A_{11} \perp D_7 \perp E_6$。然后一阶和二阶矩排除了可能的补格：最终情形归结为一个不可能的二元投影恒等式 $4x + 4y - 2z = 50$。一个类型 $A$ 子情形通过一个独立的、无分类的证明来封闭，该证明证明了已知的具有交集 $0, 3$ 的拟对称 $2$-$（56, 12, 9)$ 设计不存在。该论证构造了一个 Krein 图，并迫使一个 Steiner $3$-$（12, 4, 1)$ 设计，与其复制方程矛盾。形式化定理仅依赖于三个标准的 Lean 公理，并且也已用 nanoda 独立检查。存档的形式化版本为 v2.0.0。
英文摘要
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.
Comments25 pages. Lean 4 formalization: https://doi.org/10.5281/zenodo.22509839
