files / problems / ramsey-r55 / RESEARCH.md

15 KB · on GitHub

Research note — R(5,5)R(5,5)

Published record, fetched tonight

Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics Dynamic Survey DS1, revision 18, 24 April 2026, 149 pages, 1066 references. Local copy: compute/refs/radziszowski-ds1-rev18.pdf from https://www.cs.rit.edu/~spr/ElJC/ejcram18.pdf. The E-JC “View PDF” URL returned HTML; the RIT file is the real 585821-byte PDF.

Angeltveit–McKay, R(5,5)≤46R(5,5)\le 46, arXiv:2409.15709v2 (1 September 2025). Local copy: compute/refs/angeltveit-mckay-r55-le46.pdf. The proof is linear programming on neighbourhood excess plus a pair of independent ~30 and ~50 CPU-year gluing censuses of dense members of R(4,5,n)\mathcal R(4,5,n) for n=21,22,23,24n=21,22,23,24. The authors write that the same method at 45 would need new theory, not more of the same computer time.

Post-April-2026 screen (arXiv + the survey itself): no later accepted movement of either endpoint.

McKay’s combinatorial-data page still hosts the 328+complements file r55_42some.g6 (47888 bytes, SHA-256 067902e853d87b49bcef0d1d4c0e3bbadd238ee18bc65341b079a3ca4780eccb).

What was independently verified

  1. All 328 stored graphs, and all 328 complements, are (5,5,42)(5,5,42). None is self-complementary in the given labelling. Every stored graph has δ=19\delta=19, Δ=22\Delta=22. Edge counts on the stored half: 423 (1), 424 (7), 425 (29), 426 (66), 427 (89), 428 (77), 429 (43), 430 (16). Script: compute/verify_mckay.py. Certificate: compute/certs/mckay42_verify.json.
  2. None of the 656 graphs extends by one vertex. Neighbourhood SAT: no K4K_4 in SS, no independent 4-set in V∖SV\setminus S, 18≤∣S∣≤2418\le|S|\le 24. 31.1s, 883980 DPLL nodes, 0 models. Script: compute/extend_check.c. Log: compute/logs/extend_check.txt. This replays McKay–Radziszowski’s extension claim. It is not a proof that R(5,5)≤43R(5,5)\le 43.
  3. Paley-17 is (5,5)(5,5); Paley-41 has ω=α=5\omega=\alpha=5 and is correctly rejected. Both are sanity checks of the clique code.

What was searched and found empty

Circulants, legal degrees from R(4,5)=25R(4,5)=25. C implementation circulant_census.c; every HIT re-checked by r55lib.is_ramsey; zeros at 42 and 43 independently replayed in Python (py_circulant.py, 1167322 legal sets each).

One-flip ball of the 656. 564816 candidate flips, 4080 preserve (5,5,42)(5,5,42). Canonical 1-WL types: 194 among the 656; every surviving flip stays in those types. No new 1-WL type.

Seidel switching. Every 1-set and every 2-set on every one of the 656 graphs: zero (5,5)(5,5) results.

Cayley graphs on all six groups of order 42, inverse-closed connection sets, degrees in [17,24][17,24]. Group laws checked (check_groups.py). All six empty. Certificate: compute/certs/cayley42_census.json.

group leaves hits
C42C_{42} 1167322 0
D21D_{21} 154888897 0
C7×S3C_7\times S_3 365033 0
C3×D7C_3\times D_7 1284757 0
AGL(1,7)\mathrm{AGL}(1,7) 949786 0
C2×F21C_2\times F_{21} 106226 0

The 656 published graphs are therefore non-Cayley. This does not rule out a non-Cayley vertex-transitive graph of order 42 (Aut without a regular subgroup), and it does not rule out a 43-vertex graph with trivial automorphism group.

Involution-symmetric 43-vertex SAT. Encoder validated on n=17n=17: kissat SAT, decoded graph is (5,5,17)(5,5,17) with 58 edges (certs/involution17_model.json). The 43-vertex instances cnf/involution43.cnf (22785 vars) and cnf/involution43_slim.cnf (462 vars) both returned s UNKNOWN at 900s and 1200s. Those timeouts are not a dent and do not constrain involutions.

What this is not

Harborth–Krause already implied the cyclic half of the 43-census. The Cayley-on-all-groups half at 42, the independent non-extension replay, the 1-WL flip types, and the Seidel isolation are the residue.

Replay

cd problems/ramsey-r55/compute
python3 verify_mckay.py
./extend_check refs/r55_42some.g6
./circulant_census 43
python3 py_circulant.py 43
python3 check_groups.py

2026-08-27 — urls opened

Failed / unused: https://www.cs.rit.edu/~spr/PUBLIC/index.html returned 404 (the survey lives under ElJC/).

Independent parent replay this session: compute/replay.sh and python3 verify_mckay.py. 328+328 ok, 0 extensions, circulant 42/43 empty.

2026-08-27 — what q1 checked

Not a new bound. Independently verified tonight:

  1. Group laws for the four groups of order 44 and both groups of order 45 (q1/check_groups.py).
  2. No legal-degree Cayley (5,5)(5,5)-graph on C2×C22C_2\times C_{22}, C11⋊C4C_{11}\rtimes C_4, D22D_{22}, or C3×C15C_3\times C_{15}. Circulants at 44 and 45 empty (replay of the 17 August census). Python matched the C leaf counts on C11⋊C4C_{11}\rtimes C_4 and C3×C15C_3\times C_{15}.
  3. 4080 one-flip (5,5,42)(5,5,42) neighbours of the 656; none extend (q1/extend_flips.c).
  4. ∣Aut∣|\mathrm{Aut}| of the 656 is 11 (424 graphs) or 22 (232 graphs); no 7-cycle.
  5. No integral SRG parameters on 43 vertices with degree in [18,24][18,24]; 43≢1(mod4)43\not\equiv 1\pmod 4.
  6. C7C_7 encoder agrees with brute force on n=7n=7 and produces a (5,5,14)(5,5,14)-graph. The 42- and 43-vertex slim instances timed out. Those timeouts are not a dent.

Cert: compute/q1/certs/q1_summary.json. Replay: cd compute/q1 && ./run_all.sh.

2026-08-29 — q3 order-7 certificates

No new Ramsey bound. The published interval remains 43≤R(5,5)≤4643\le R(5,5)\le46.

The q2 prime-order encoder was reused unchanged. Checked certificates now exclude all six order-7 permutation cycle counts 7c143−7c7^c 1^{43-7c} on 43 vertices. Direct DRAT proofs cover eight fixed-neighbour representatives for c=1,…,5c=1,\dots,5; complementation pairs kk with c−kc-k. For c=6c=6, a local DRUP exhausts 787 possible 21-vertex neighbourhoods and 787 conquer DRUPs refute the original q2 CNF under those assignments. Certificate: compute/q3/certs/q3_summary.json.

By Cauchy's theorem, combining q2 and q3 leaves only 2, 3, and 5 as possible prime divisors of the automorphism-group order of a hypothetical (5,5,43)(5,5,43)-graph. This does not rule out such a graph and does not move an endpoint. The maximum-cycle order-2, order-3, and order-5 instances still time out, and their other cycle types remain incomplete.

Proof-format and case-splitting references opened during the certificate work:

2026-08-29 — q4 leftover 2/3/5

No new Ramsey bound. The published interval remains 43≤R(5,5)≤4643\le R(5,5)\le46.

Fetched again before searching:

q2's encoder was reused unchanged. Checked certificates now exclude the order-5 cycle types 561135^6 1^{13} and 57185^7 1^8 on 43 vertices (three stored DRATs; complementation covers the paired neighbour counts). Independent replay: compute/q4/logs/replay_direct.txt. The maximum-cycle order-2, order-3, and order-5 formulas still time out, as do the other leftover representatives that were run. This does not move an endpoint.

2026-08-29 — leftover SAT after 5^6 and 5^7

Fetched again before searching:

q2's encoder was reused unchanged. One new checked certificate excludes the order-5 cycle type 541235^4 1^{23} at k∈{0,4}k\in\{0,4\} on 43 vertices (stored as compute/q5/certs/proofs/p5_c4_k4.drat.xz). Independent replay: compute/q5/logs/replay_direct.txt. All five maximum-cycle formulas still time out at thirty minutes, as do the other leftover representatives that were run. This does not move an endpoint.

2026-08-29 — leftover SAT after 5^4 at k=4

Fetched again before searching:

q2's encoder was reused unchanged. One new checked certificate excludes the order-5 cycle type 551185^5 1^{18} at k∈{2,3}k\in\{2,3\} on 43 vertices (stored as compute/q6/certs/proofs/p5_c5_k2.drat.gz). Independent replay: compute/q6/logs/replay_direct.txt. 555^5 at k=1k=1 timed out at sixty minutes. The other leftover representatives that were run also timed out. This does not move an endpoint.

2026-08-29 — leftover SAT after 5^5 at k=2

Fetched again before searching:

q2's encoder was reused unchanged. 551185^5 1^{18} at k=1k=1 returned kissat UNSAT after 7575s. The trimmed DRAT is 4123082549 bytes (SHA-256 d1f770b0b7c50ca2bb08a4d8872b4bc21a17bda8401cdef9360267e071df8574) and was not stored. The independent check was stopped at wrap. This is not an independently replayed certificate and does not move an endpoint.