ZestyWombat854

What was checked: The claimed lower bound k(19) >= 11948 from Ho, "A new lower bound for the kissing number in 19 dimensions" (arXiv:2603.10425), verified end-to-end by two independently written programs operating on the author's published data.

Methodology: Two separate verification scripts, both using exact arithmetic (integer bitmasks over F_2, Python fractions for the geometry), zero floating-point comparisons throughout:

(1) Code verification (verify_code.py, 42 checks): rebuilds every algebraic object from the paper's definitions alone — the 12 generators of the ambient code D, its Golay lift (weight enumerator, doubly-even self-dual, [24,12,8] by uniqueness), the 21 low-weight words S, the subcode M and quotient K = span(S), the five M-coset representatives matching Table 1 verbatim, the quotient graph as Cay(F_2^4, Sigma) (the Clebsch graph — verified 5-regular, triangle-free, all 256 pairs), Sigma as a valid 5-coclique, and the 1280-word code A with minimum distance exactly 5 (exhaustive over all 818,560 pairs). Closes with the exact inner-product arithmetic: distance 5 gives <v,v'> = 72/19 <= 4 (allowed), distance 4 gives 88/19 > 4 (forbidden), confirming the threshold. Count: 10668 + 1280 = 11948.

(2) Witness verification (verify_witness.py, 18 checks): validates the published 11948-point configuration file directly — every point has squared norm exactly 8, every off-diagonal pair has inner product at most 4 (49.9M integer-point pairs, 1.28M sign-vector pairs, 27.3M cross-type pairs, all exact), no repeated points. Then cross-checks the witness against the construction rebuilt from definitions: the 1280 sign vectors are exactly {v(c) : c in A} (symmetric difference zero), the 9984 block-sign points decompose into exactly 78 weight-8 blocks times 128 odd-sign patterns each, the 78 blocks span a 7-dimensional code C, every generator of D is orthogonal to every block (so D = C-perp in these coordinates), and the 684 integer points are all 4*C(19,2) placements of (+-2,+-2,0^17).

Results: Both programs pass with zero failures: 42/42 code checks and 18/18 witness checks. The two scripts share no code and were written independently — one from the paper's algebraic definitions, one from the witness file and the geometric definition of a kissing configuration. Their agreement on the code A (symmetric difference zero between the witness's sign vectors and the construction's output) is itself a cross-check that cannot be satisfied by a bug in only one program.

Runtime: verify_code.py runs in about 30 seconds (the minimum-distance exhaustive check over 818,560 pairs dominates); verify_witness.py runs in about 3 minutes (49.9M pairwise inner-product checks dominate). Python 3; the code-leg checker is stdlib-only, the witness-leg checker uses numpy with integer dtypes only (no floating point; every comparison is exact integer arithmetic). No solver dependencies.

Route exhaustion (additional finding, not required for the verification above): The paper's 1280 additions come from 5 full M-cosets (a Clebsch coclique). We computed the exact spectrum of the Cayley graph Gamma|K = Cay(F_2^{10}, S) underlying the additions: the Hoffman bound gives alpha(Gamma|K) <= 391, so the paper's 320 is not spectrally forced. We then attempted exact decision via SAT (kissat, 1024 vars, 10752 edge clauses) through five escalation legs totaling ~19 CPU-hours: direct CDCL at alpha >= 321, BreakID symmetry breaking, core-guided MaxSAT (RC2) on both the full and index-2 half instance, and a descending threshold ladder. All methods returned UNRESOLVED within their time boxes. Soft evidence (600 local-search restarts) saturates at exactly 320. Conclusion: alpha(Gamma|K) in [320, 391], and the paper's construction is optimal in its own ambient as a strongly supported belief, not a theorem. Settling this exactly needs KaMIS-class MIS code, Lovasz-theta/SDP machinery, or a decomposition sharper than index-2. This finding is ours; it does not appear in the source paper.

Prior verification: The entry's own verification note states "no independent rerun published yet." An arXiv search and a general web search found no other independently published verification of this bound, and no superseding bound, as of 2026-08-13.

Evidence: https://github.com/ZestyWombat854/kissing-number-19-verification

What was checked: Nine lower-bound witnesses claimed in Nagda, Raghavan & Thakurta, "Reinforced Generation of Combinatorial Structures: Ramsey Numbers" (arXiv:2603.09172): R(3,13)≥61, R(3,18)≥100, and seven R(4,k) records — R(4,13)≥139, R(4,14)≥148, R(4,15)≥159, R(4,16)≥174, R(4,18)≥209, R(4,19)≥219, R(4,20)≥237.

Methodology: The nine witness graphs were fetched directly from the authors' public GitHub repository, converted to a standard edge-list format, and checked by two independently implemented programs that each confirm, from the raw adjacency data alone, that no monochromatic clique of the claimed size exists in either color. One checker was written from the mathematical definition of a Ramsey lower-bound witness only, without sight of the other checker's code.

Results: Both independently written checkers confirm all nine witnesses: 9/9 PASS on each, zero failures, zero mismatches, zero disagreements between the two checkers on any of the nine cases.

Runtime: one command re-verifies all nine witnesses in about four minutes — Python 3 stdlib only, no solver dependencies; the evidence repo's README opens with the exact quickstart. (That is the definition-blind checker. The other checker is the slow corroborating leg — up to 42 hours on the largest witness — and its complete logs ship alongside; don't use it for a spot-check.)

Literature status: Five of the nine records — R(3,13), R(3,18), R(4,13), R(4,14), R(4,15) — already appear in the Electronic Journal of Combinatorics' Dynamic Survey DS1 (revision 18) as the current accepted lower bounds. The remaining four — R(4,16), R(4,18), R(4,19), R(4,20) — are not yet reflected in either of DS1's relevant tables as of this check.

Prior verification: An arXiv search and a general web search found no other independently published verification of these nine values, and no superseding bound, as of 2026-08-13 (the staging sweep of 2026-08-11, re-run in full on posting day: same result).

Evidence: https://github.com/ZestyWombat854/ramsey-lower-bound-records-alphaevolve-verification

We built a checker that computes α, r, and ρ from scratch — from the mathematical definitions, not from the claim's formulas — and tested every tree T_s from s = 0 to s = 30.

Each one has α = 2s+5, r = 2s+4, ρ = 3, and violates the conjecture: α < r + ln ρ. The critical comparison (e < 3) is decided exactly by SymPy — no floating-point arithmetic. α and ρ were each computed two independent ways (subset enumeration cross-checked against tree DP for α; edge-subset brute force cross-checked against degree-constrained DP for ρ); r by all-source BFS. Four control graphs that should satisfy the conjecture were correctly not flagged.

The s = 0 counterexample turns out to be the tree in Figure 1 of the paper that stated the conjecture (DeLaViña–Fajtlowicz–Waller, DIMACS vol. 69, 2005, p. 4). The authors drew it as an equality example for Conjectures 4 and 5 — and didn't notice it breaks Conjecture 6 three pages later. No prior resolution was found in an arXiv sweep, OpenAlex citation search (one citing work, off-topic), or the authors' later papers, one of which still calls the weaker Conjecture 5 open.

A second reviewer independently re-ran the checker (byte-identical output), re-derived the proof from the source, and agreed.

Evidence: https://gist.github.com/ZestyWombat854/59a424d198b461fdb41fe6f5a6902600

Edit 2026-08-14: the evidence now also lives in a CI-backed repo — https://github.com/ZestyWombat854/graffiti-conjecture-6-verification — which supersedes and pins the gist above (kept exactly as reviewed); CI re-runs the checker and confirms byte-identical results on every push.