2026/07/29 by Samuil Petkov
Mathematics · #math.CO #math.SP #msc:05C50 #msc:05C12 #msc:05E30
28 pages. Exact computations and Lean 4.31 certificates
arxiv created 2026/07/29 · arxiv updated 2026/07/31
WOW-284 asserts that the minimum dual degree of every connected graph of order at least three and girth at least five does not exceed the negative of its least distance eigenvalue. We refute it with exact counterexamples of orders 38,39,40,42, and 50, and develop a structural theory of the failure. For a connected k-regular graph of girth at least five and diameter three, we prove δ^*(G)+λmin(D(G))=2k-2-maxθ≠ k(θ+1)2. Here θ ranges over the nonprincipal adjacency eigenvalues. We further prove that every regular strict counterexample has degree at least six and diameter at most four, while diameter four forces degree at least ten. We solve the associated one-variable nonbacktracking linear program exactly, including optimizer rigidity. For regular strict counterexamples of diameter three, the optimizer yields a positive-semidefinite slack matrix whose integral excess gives the stronger bound |V(G)|≤\lfloor 3(k+2)2(k2+3)/(18k+41)\rfloor; this follows from a three-to-one quantization theorem for the integral excess. The slack matrix's principal minors also recover local cycle constraints. In particular, regular degree-six counterexamples have order at most 50, and at the degree-six, order-50 boundary the associated signed complement is necessarily disconnected. We determine the distance spectra of one- and two-vertex punctures of Moore graphs and establish a uniform deletion-stability bound: every deletion of at most five vertices from the Hoffman--Singleton graph remains a strict counterexample, whereas an explicit six-vertex deletion does not. All theorem-level computations use exact arithmetic. Lean 4.31 kernel-checks the explicit 50-vertex Hoffman--Singleton counterexample at graph level, finite spectral certificates at orders 38,39,40,42, and the analytic LP optimum and rigidity for every integer k≥4.