Structural rigidity at the R(5,5) lower-bound frontier: flip-ball exhaustion, window-SAT, and DRAT-certified prescribed-automorphism results

With DRAT-certified UNSAT proofs for every symmetry claim — make verify checks them all. The Ramsey number R(5,5) satisfies 43 ≤ R(5,5) ≤ 46 (Exoo 1989; Angeltveit–McKay, arXiv:2409.15709), and McKay–Radziszowski conjecture R(5,5)=43, supported by the 656 known Ramsey(5,5,42) graphs, none of which extends to 43 vertices. The best public near-misses at n=43 are two edge-colorings of K₄₃ with exactly two monochromatic K₅s (Exoo, unpublished; Molnár–Molnár–Toroczkai, arXiv:1801.06620). A coloring with zero would prove R(5,5) ≥ 44. This repository documents three machine-checked structural results about that frontier (no witness was found; everything here is consistent with R(5,5)=43): # result status R1 Both public 2-defect K₄₃ colorings are rigid: exhaustive flip search to Hamming radius 4 (≈2.76×10¹⁰ configurations each), ≈6.8×10⁹ annealed focused-flip proposals, and 735 coordinated window-rewrite SAT instances (≤528 free edge variables) never reach fewer than two monochromatic K₅s exhaustive + solver-reported R2 42 prescribed-automorphism instances UNSAT for (5,5,n), n = 43…47. Corollary: any Ramsey(5,5,43) graph has no automorphism of prime order ≥ 17 — its automorphism group order is {2,3,5,7,11,13}-smooth DRAT-certified, 42/42 R3 First extension-defect spectrum of the 656-graph census: the minimum number of monochromatic K₅s over one-vertex extensions has floor 2, attained by exactly 4 census graphs; no census graph extends with 0 or 1 defects search upper bounds The orbit-collapse method behind R2 is classical (Radziszowski–Kreher, J. Graph Theory 12, 1988; SAT symmetry-breaking à la Itzhakov–Codish/Heule); the certified applied statements at n = 43–47 are, to our knowledge after an adversarial prior-art review (2026-07-10), new. Full write-up: PAPER.md. Verify the certificates make fetch-proofs # pulls the 8 large DRAT proofs (~1.4 GB) from the v1.0 release make verify # builds drat-trim, then checks all 42 CNF+DRAT pairs Each instance orbit_n{N}_p{P}_k{K} asserts: no (5,5,N) Ramsey graph is invariant under an order-P automorphism with K P-cycles. The CNF is regenerable from the canonical encoder: python3 code/src/orbit_sat.py N P K --dimacs out.cnf. Proof/CNF SHA256 hashes, solver (kissat 4.0.4) and checker (drat-trim) versions: certificates/manifest.json. 34 of 42 proofs live in-tree; the 8 largest (up to 631 MB uncompressed) are attached to the v1.0 release (GitHub 100 MB tree limit). Reproduce the searches (R1, R3) Two independent (5,5,n) verifiers (code/src/verify55.c, code/src/verify55.py) gate everything (code/src/g0_gate.py, 2,858-instance agreement). Flip-ball exhaustion: code/src/flipball43.c; annealer: code/src/sa55.c; window-SAT: code/src/sat_polish.py; extension spectrum: code/src/minext.c. Raw run receipts (including all 204 worker logs from the 192-core farm run) are in receipts/; the near-miss seed data and the full 656-graph census with BLISS canonical forms are in data/. Honest scope R1's 735 window-UNSATs are solver-reported (kissat), not proof-logged; 944 larger windows hit the time budget and remain open (resolution boundary ≈530–630 free variables). R3 values are local-search upper bounds. Orbit coverage is the certified list, no more: at n=43 the corollary is complete for all primes ≥ 17; orders ≤ 13 are partially covered (see receipts/orbit_coverage.json for every open (p,k) case). None of this proves R(5,5)=43 — it quantifies why the standing frontier resists.