Tagewerk XXXV

Kernel-attested audit: the srg(1666,105,0,7) non-existence proof does not decide the case (Belousova-Makhnev-Tokbaeva 2026)

An audit, in a domain new to the ledger -- spectral / algebraic graph theory (strongly regular graphs) -- of a 2026 non-existence proof, independently re-decided from first principles and kernel-attested. Belousova, Makhnev & Tokbaeva (Vestnik Perm. Univ. 1(72), 2026, 29-34) prove that srg(1666,105,0,7) does not exist by ruling out its bipartite double, the distance-regular graph with intersection array {105,104,98,7,1;1,7,98,104,105} (3332 vertices), via triple intersection numbers. srg(1666,105,0,7) is the smallest feasible triangle-free srg with mu=7 (Biggs' k=49s^2+49s+7 family, s=1) -- a long-standing feasible-but-open parameter set, beyond every published table. Leibniz reconstructs the whole argument in exact rational arithmetic from the array alone: Lemmas 1-3 reproduce exactly (the intersection numbers, the dual eigenmatrix, the Krein parameters, the unique Lemma-2 triple solution and the one-parameter Lemma-3 family r1 in {0..7}), catching one typo (Lemma 1 prints p^2_33=543; it is forced to 1461 by duality and a row sum). But the proof of Theorem 1 does NOT establish non-existence: its contradiction compares two computations of the mean lambda of the auxiliary graph Lambda (the distance-2 graph on Gamma_2(u), p^2_22=1461-regular on 1560 vertices), and with correct arithmetic BOTH equal 1999388/1461. The printed gap (1362.905 vs 1368.09) is an artifact of two compensating errors -- using 104 for the true non-neighbour count 1560-1-1461=98, and dividing by 1560 instead of the degree 1461 -- with the structural identity [222]+[224]=1364+97=1461=p^2_22 forcing S1=S2. The triple-intersection method leaves the array feasible: every metric base triple (with all 81 zero-Krein equations) has a non-negative integer solution, and the all-distance-2 config has exactly 8. This is corroborated by the canonical tool the authors cite, sage-drg (check_feasible clean; all deeper checks pass; tripleSolution_generator(2,2,2) -> 8 solutions; no zero-solution config; it too reports p^2_33=1461), and by three further independent from-scratch reconstructions. The Lean 4.31 kernel re-decides the finite core (plain decide): the two mean-lambda sums are equal, the structural identity, the paper's 104 manufactures the gap, all 8 Lemma-3 witnesses satisfy every marginal + zero-Krein equation + non-negativity, the Lemma-2 witness is valid, and r1=8 is rejected (a negative control). #print axioms at most [propext]; no native_decide, no sorry. Report-only, audit tier. CONCLUSION: the given proof does not decide the parameter set; srg(1666,105,0,7) should be treated as OPEN. This is an audit of a proof's validity, NOT a claim that the graph exists or does not exist. LLMs propose nothing; exact arithmetic and the kernel decide.