{"id":"9ba82224-b774-4a2c-aa3e-e05dc3a74183","arxiv_id":"2607.27452","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":6.5,"correctness_risk":"low","formal_verification":"partial","parameter_count":0,"one_line_summary":"WOW-284 fails on explicit graphs of orders 38,39,40,42,50; regular strict counterexamples need degree ≥6 and diameter ≤4, with exact LP order bounds and Hoffman–Singleton deletion radius five.","lead":"A 1998 graph-theory conjecture (WOW-284) is false: explicit graphs of orders 38–50 violate the claimed dual-degree vs. distance-eigenvalue inequality. The paper also pins down when regular counterexamples can exist and how stable they are under vertex deletion.","discovery_kind":"extension","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified","rationale":"The reader correctly separates the easy, self-contained existence refutation (HS and descendants, Lean-checked) from the longer obstruction hierarchy that cites external enumerations. Those enumerations are the weakest assumptions in the manuscript, yet they are not load-bearing for the claim that WOW-284 is false. The diameter-three score identity (Theorem 3.1), the exact LP ceiling (Theorem 5.3, also Lean-checked), and the deletion-stability radius are additional structural contributions whose correctness is independent of the low-degree case split. No internal inconsistency or hidden analytic gap was found that would overturn existence or the main regular score calculus. Hence the ACCEPT / HIGH verdict stands; the concrete test above is only a minimal independent sanity check on the flagship example.","tokens_in":31268,"tokens_out":527,"duration_ms":9980,"concrete_test":"Independently recompute λ_min(D) and δ* for the archived graph6 of the Hoffman–Singleton coordinate model (or any standard HS realization) by exact rational characteristic polynomial / LDL^T; confirm Φ=3>0. This single check reconfirms the existence half of the strongest claim without any cage census or λ_min≥-2 classification.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is the explicit refutation of WOW-284. That claim is independently secured by the Hoffman–Singleton graph (and its Lean-checked coordinate model) together with the diameter-two Moore score formula of Theorem 2.2; the smaller exact certificates at orders 38–42 are likewise machine-audited. The reader’s cited soft spots—Meringer’s (5,5)-cage census inside Theorem 4.2 and the Cameron–Goethals–Seidel–Shult / CRS classification of regular graphs with λ_min≥-2 inside the r≤0 analysis of Theorem 6.1—are real dependencies, but they underwrite only the low-degree/order obstruction side of the structural theory. A gap there would reopen whether every regular strict counterexample has degree ≥6 (or the three-to-one excess bound), not whether counterexamples exist. Because the paper’s primary scientific act is the existence refutation, and that act does not rest on those classifications, there is no load-bearing concern that threatens the strongest claim.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper refutes Fajtlowicz’s WOW-284 conjecture by exhibiting connected girth-at-least-five graphs with Φ(G)=δ*(G)+λ_min(D(G))>0 at orders 38, 39, 40, 42, and 50, anchored by the Hoffman–Singleton graph and explicit descendants (Anstee–Robertson cage, punctures, second subconstituents). For connected k-regular girth-≥5 diameter-3 graphs it proves the exact score identity Φ(G)=2k−2−max_{θ≠k}(θ+1)^2, so strict failure is equivalent to confinement of the nonprincipal adjacency spectrum in the open shifted window (−1−√(2k−2),−1+√(2k−2)). It then develops degree/diameter obstructions (regular strict counterexamples have k≥6 and diam≤4; diam 4 forces k≥10), solves the associated one-variable nonbacktracking LP exactly with optimizer rigidity, and derives an integral-slack three-to-one order bound, local cycle sieves, and a disconnected signed-complement constraint at the (6,50) boundary. Parallel sections give exact distance spectra of Moore punctures and a sharp Hoffman–Singleton deletion radius of five. Theorem-level numerics use exact arithmetic; Lean 4.31 kernel-checks the 50-vertex certificate, finite spectral certificates at 38–42, and the analytic LP optimum/rigidity for all k≥4.","tokens_in":31439,"tokens_out":1376,"duration_ms":41580,"significance":"If correct, this is a clean, constructive settlement of a recorded Graffiti/distance-spectrum conjecture, together with a usable structural calculus for when and why the inequality fails. The diameter-three score formula, exact LP ceiling B_k with rigidity, and integral-slack hierarchy are of independent interest beyond the conjecture. Strengths that raise the contribution above a bare counterexample list include: explicit coordinate models and exact spectra; reproducible exact-arithmetic certificates; a sharp deletion-stability theorem for Hoffman–Singleton; and a sorry-free Lean 4.31 development that kernel-checks the principal 50-vertex graph-level certificate, the small-order spectral certificates, and the LP optimum/rigidity for every integer k≥4. The work is carefully scoped about what is and is not formalized.","major_comments":[{"comment":"Theorem 4.2’s exclusion of degree 5 in diameter three rests on Meringer’s isomorph-free census of the four (5,5)-cages and exact distance spectra of fixed graph6 records (and, for n=32, a compressed-layer interlacing argument). The existence refutation does not need this step, but the paper’s stated main conclusion that every regular strict counterexample has degree ≥6 does. Please make the logical dependence explicit in the theorem statement or proof, pin the four graph6 strings (or canonical labels) in the text or a table, and state clearly that the degree-five case is certified by exhaustive check of that finite list rather than a classification-free argument.","section":"Theorem 4.2"},{"comment":"In the r≤0 analysis of Theorem 6.1, the argument invokes the Cameron–Goethals–Seidel–Shult / Cvetković–Rowlinson–Simić classification of connected regular graphs of order >28 with least eigenvalue ≥−2 (line graphs or cocktail-party graphs), then derives contradictions via irreducibility and dimension-mod-4 constraints. This underwrites the three-to-one excess bound and the degree-six order-≤50 corollary. The citations are appropriate, but the write-up should isolate this external classification as a named hypothesis in the proof tree (what fails if one only assumes the classification up to a larger order, etc.) so that the integral-slack consequences are auditable independently of the existence counterexamples.","section":"Theorem 6.1"}],"minor_comments":[{"comment":"Section 10 already delimits the Lean scope well; a one-sentence cross-reference in the introduction (what is kernel-checked vs. only exactly audited in Python) would help readers who stop at the main theorems.","section":"Section 1 / Section 10"},{"comment":"In Theorem 2.4, the H_39 row reports an exact strict lower bound via positive-definiteness of 6D+35I rather than the exact least eigenvalue. The prose explains this, but the table header “λ_min(D(G))” is slightly misleading; consider “bound on λ_min” or a footnote mark in the table.","section":"Theorem 2.4"},{"comment":"Corollary 6.7 and the comparison table of unadjusted diameter-three bounds are useful; adding the parity improvements for odd k directly into that small table would avoid a second prose pass.","section":"Corollary 6.7"},{"comment":"Several script names are cited as independent audits (e.g., verify_proof_audit_02_two_sided_lp.py). For journal permanence, ensure the arXiv ancillary or a DOI-backed release tags the exact commit/release (v2.2.8 is mentioned) and that graph6/edge-list inputs are immutable.","section":"Section 10"},{"comment":"Minor notation: δ* and d* are introduced cleanly, but Φ(G) appears before it is formally defined in some readers’ skim path (abstract vs. §1). A parenthetical in the first paragraph of §1 is enough.","section":"Section 1"}],"recommendation":"minor_revision","confidential_remarks":"The existence refutation is solid and essentially settled by Hoffman–Singleton plus the Moore score formula; I would not ask for a rewrite of that core. The only reason I chose minor_revision rather than accept is that two advertised structural conclusions (degree ≥6; the sharp integral order bound) genuinely lean on external finite classifications, and the manuscript should present those dependencies with the same explicitness it gives the Lean scope. No concerns about novelty disclosure or citation behavior. Good fit for a combinatorics journal that accepts computer-assisted and formally verified components."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The punchline is simple: WOW-284 is false, and they prove it with exact graphs (orders 38–42 and Hoffman–Singleton at 50), not with asymptotics. The short Moore argument already kills the conjecture for k>3, and the paper says so up front. What is actually new is the package around that fact: the diameter-three score formula equating Φ to an adjacency window, the degree/diameter trichotomy for regular strict counterexamples, the exact one-variable nonbacktracking LP with rigid optimizer, the integral-slack three-to-one order bound, the sharp HS deletion radius of five, and Lean-checked certificates for the flagship example, the small spectra, and the LP.\n\nThat is real work. Theorem 3.1 is the right transfer identity under girth ≥5 and diameter 3. The LP duality/rigidity writeup is careful. Deletion stability for punctured Moore graphs is clean and useful. Shipping exact arithmetic plus a graph-level Lean check of the 50-vertex certificate is stronger reproducibility than most of this literature bothers with. Citations look appropriate (Graffiti/Aouchiche–Hansen, Moore/cage sources, Nozaki, CRS/root-system material).\n\nSoft spots, in proportion: the low-degree obstruction side leans on Meringer’s (5,5)-cage census and the λ_min ≥ −2 classification when analyzing the slack graph. Those are standard external inventories, not hidden fitting, and they underwrite “degree ≥6 / order windows,” not existence of counterexamples. The degree-six order-50 boundary is constrained but not eliminated; the paper is honest about that. They do not claim 38 is minimal or that the list is complete.\n\nWho it is for: people in distance spectra, cages/Moore graphs, and spectral extremal graph theory. A serious referee should see it. I would bring it to reading group and cite the score formula, LP ceiling, and deletion radius if I were working nearby. Send it to peer review.","headline":"Clean explicit refutation of WOW-284 plus a real structural package; the easy Moore counterexample is old news, the rest is the paper.","tokens_in":32116,"tokens_out":513,"would_cite":true,"duration_ms":15132,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["05C50","05C12","05C35","05E30"],"pacs":[],"model":"grok-4.5","headline":"WOW-284 is false: connected girth-at-least-five graphs can have minimum dual degree strictly larger than the negative of their least distance eigenvalue, with exact counterexamples from order 38 up through the 50-vertex Moore graph and a fu","keywords":["distance spectrum","dual degree","Moore graph","WOW-284","nonbacktracking LP","girth five","deletion stability","slack matrix"],"falsifier":"Exhibit a single connected 5-regular graph of girth at least five whose distance matrix has least eigenvalue strictly greater than −5, or a 6-regular girth-five graph on more than 50 vertices whose non-principal adjacency eigenvalues all lie inside (−1−√10,−1+√10); either object would break the stated obstructions.","tokens_in":32079,"feed_emoji":"📉","tokens_out":1288,"duration_ms":29843,"temperature":0.7,"pith_summary":"The paper refutes a long-standing graph conjecture that tied two simple spectral-and-degree quantities: for every connected graph on at least three vertices with no triangles or 4-cycles, the smallest average-neighbour-degree was supposed never to exceed the negative of the smallest eigenvalue of the distance matrix. Explicit counterexamples exist at orders 38, 39, 40, 42 and 50, beginning from the classical diameter-two Moore graphs and their vertex deletions. For regular graphs the failure is completely characterized when the diameter is three: it is equivalent to every non-principal adjacency eigenvalue lying inside a fixed open interval around −1. From that identity the paper derives hard lower bounds on degree, upper bounds on diameter and order, an exact one-variable linear-programming ceiling, and a positive-semidefinite slack matrix whose integral excess forces a three-to-one order bound. It also proves that deleting up to five vertices from the 50-vertex Moore graph preserves the counterexample property, while some six-vertex deletion destroys it. The result matters because it replaces an attractive universal inequality with a sharp spectral window, quantitative order limits, and a deletion-stability radius that can be checked exactly.","feed_headline":"Conjecture on graph distances fails at order 38","feed_subtitle":"Exact counterexamples and a spectral window explain when minimum dual degree beats the least distance eigenvalue","key_machinery":"The diameter-three score identity D=3J+(k−3)I−2A−A², which converts the dual-degree-plus-distance-eigenvalue gap into a two-sided window on the adjacency eigenvalues, together with the optimal non-backtracking polynomial whose slack matrix is positive-semidefinite and whose integral excess quantizes to the three-to-one order bound.","core_discovery":"WOW-284 fails: there exist connected graphs of girth at least five with Φ(G)=δ*(G)+λ_min(D(G))>0. For connected k-regular graphs of girth at least five and diameter three the score collapses to the closed formula Φ(G)=2k−2−max_{θ≠k}(θ+1)^2, so strict counterexamples are exactly those whose non-principal adjacency spectrum lies in the open interval (−1−√(2k−2),−1+√(2k−2)). Every regular strict counterexample has degree at least six and diameter at most four; diameter four forces degree at least ten. Regular degree-six counterexamples have order at most 50.","pith_inferences":["The same slack-matrix minors that recover 5-cycle counts should extend to a practical computational sieve for hunting (or ruling out) the remaining degree-6 order-50 candidates without full spectrum computation.","Because the LP optimum is rigid and graph-independent, the same one-variable certificate can be reused as a black-box filter inside any search for irregular or larger-girth distance-spectrum counterexamples.","The sharp five-vertex deletion radius for the 50-vertex Moore graph suggests a broader stability programme: measure how far other extremal cages can be punctured before their distance-score sign flips.","If a degree-10 diameter-4 regular counterexample exists, the endpoint-neighbourhood Rayleigh bound already forces it near the edge of feasibility, so a short computer search in that narrow band could finish the regular trichotomy."],"forward_implications":["No regular strict counterexample of degree ≤5 exists, and every regular one has diameter 2, 3 or 4 (diameter 4 only for degree ≥10).","Regular diameter-three counterexamples obey the explicit order ceiling ⌊3(k+2)²(k²+3)/(18k+41)⌋, giving windows n≤50,74,108,150 in degrees 6–9.","Every deletion of at most five vertices from the 50-vertex degree-7 Moore graph remains a strict counterexample; the universal radius is exactly five.","At the unresolved 6-regular order-50 boundary the associated signed complement must be disconnected and the (−2)-multiplicity of the adjacency matrix is at most 20.","One- and two-vertex punctures of any Moore graph of diameter two have completely determined distance spectra and remain counterexamples for all realizable degrees ≥5 or ≥6 according to the puncture type."],"fun_headline_variants":["WOW-284 fails with exact counterexamples at order 38","Girth-five graphs beat dual degree versus least distance eigenvalue","Regular counterexamples need degree ≥6 and diameter ≤4","Diameter-three score collapses to 2k−2−max(θ+1)²","Five-vertex Hoffman–Singleton deletions remain strict counterexamples"],"cache_read_input_tokens":128,"weakest_assumption_plain":"The low-degree exclusion for regular counterexamples rests on complete external enumerations of a handful of small cages and on the classical classification of regular graphs whose smallest adjacency eigenvalue is at least −2; if either inventory is incomplete the degree-five and slack-graph arguments reopen.","fun_headline_variants_meta":{"raw":{"variants":["WOW-284 fails with exact counterexamples at order 38","Girth-five graphs beat dual degree versus least distance eigenvalue","Regular counterexamples need degree ≥6 and diameter ≤4","Diameter-three score collapses to 2k−2−max(θ+1)²","Five-vertex Hoffman–Singleton deletions remain strict counterexamples"]},"model":"grok-4.5","effort":"low","cost_usd":0.005852,"raw_usage":{"total_tokens":1693,"prompt_tokens":1022,"num_sources_used":0,"completion_tokens":79,"cost_in_usd_ticks":58524000,"prompt_tokens_details":{"text_tokens":1022,"audio_tokens":0,"image_tokens":0,"cached_tokens":128},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":592,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":1022,"tokens_out":79,"duration_ms":10869,"temperature":1.0,"reasoning_tokens":592,"cache_read_input_tokens":128,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-31T00:28:40.378772+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Exhibit a single connected 5-regular graph of girth at least five whose distance matrix has least eigenvalue strictly greater than −5, or a 6-regular girth-five graph on more than 50 vertices whose non-principal adjacency eigenvalues all lie inside (−1−√10,−1+√10); either object would break the stated obstructions.","supporting_citations":[],"review_version":1}