--- title: "No 26-point four-term-AP Ramsey set has primitive diameter at most 36" date: 2026-09-03 version: "0.1.0-candidate" doi: 10.5281/zenodo.22286322 pdf: https://github.com/ipitchford/ap4-ramsey-diameter-36/releases/download/v0.1.0-candidate/ap4-ramsey-diameter-36-paper-v0.1.0-candidate.pdf repository: https://github.com/ipitchford/ap4-ramsey-diameter-36 archive: https://zenodo.org/records/22286322 license: CC0-1.0 status: unrefereed (internally replayed; not peer reviewed, not independently reproduced, not formally verified) --- # No 26-point four-term-AP Ramsey set has primitive diameter at most 36 ## Summary Take some of the integers from 1 to 37 and colour each chosen number red or blue. A set is called four-term-AP Ramsey if every such colouring contains four equally spaced chosen numbers of one colour. Ronald Graham exhibited a 27-number set with this property. This anonymous, unrefereed computer-assisted candidate proves that no set of 26 numbers inside the same interval can work. In symbols, $$ v_{2,4}([37])=27. $$ The diameter limit is essential. This finite theorem does not determine the minimum over all finite integer sets, usually written $W^*(4)$, and it does not answer the two asymptotic questions in AIM Problem 1.9. ## Summary for specialists For $S\subseteq[37]$, let $H_4(S)$ be the 4-uniform hypergraph whose edges are the nonconstant four-term arithmetic progressions contained in $S$. The release establishes that the least $|S|$ for which $H_4(S)$ fails Property B is 27. The lower certificate is a 1,579-variable, 5,761-clause CNF. Sinz counters enforce $|S|=26$; indicator variables encode the 210 four-term progressions in $[37]$; and 2,012 audited colouring cuts impose necessary conditions on any non-2-colourable selected set. A retained DRAT refutation proves the resulting formula unsatisfiable. The upper certificate directly encodes the 98 progressions in Graham's 27-point set as a 27-variable, 196-clause 2-colourability instance and supplies a separate DRAT refutation. Every cut and every clause is semantically reconstructed before proof checking. The release also checks 28 explicit positive colourings, exhausts a small 512-subset oracle, recomputes a distinct 21,329-candidate replacement neighbourhood, and requires fifteen hostile mutations to fail closed. ## Technical account For a finite integer set $X$, write $\mathrm{AP}_4(X)$ for the hypergraph with edges $$ \{a,a+d,a+2d,a+3d\}\subseteq X,\qquad d>0. $$ The set $X$ is four-term-AP Ramsey when every map $X\to\{0,1\}$ is constant on at least one edge. Define $$ v_{2,4}([N])=\min\{|X|:X\subseteq\{1,\ldots,N\}\text{ is four-term-AP Ramsey}\}. $$ For the lower bound, one Boolean variable $y_i$ records whether $i\in[37]$ is selected, and sequential counters require exactly 26 selected points. For each four-term progression $e$, a variable $z_e$ is constrained by $$ z_e\longleftrightarrow\bigwedge_{i\in e}y_i. $$ Given a complete red-blue colouring $c$ of $[37]$, let $M(c)$ be its set of monochromatic progressions. Any Ramsey set selected from $[37]$ must contain at least one edge of $M(c)$, because a colouring of the selected set extends to the whole interval. The clause $$ \bigvee_{e\in M(c)}z_e $$ is therefore necessary for every candidate. Crucially, even a subset of valid colouring cuts remains a sound necessary-condition system: if that system is unsatisfiable, no 26-point Ramsey set exists. The released 2,012-cut master formula is unsatisfiable by its checked DRAT proof. For the upper bound, the displayed set $$ \{1,4,7,8,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,30,31,34,37\} $$ has 98 four-term progressions. Its direct 196-clause colourability CNF has a separate checked DRAT refutation, so the set is Ramsey. Monotonicity rules out all smaller subsets once exact size 26 has been excluded, proving the equality. If a 26-point Ramsey set had primitive affine diameter at most 36, translation and division by the gcd of its differences would place an equivalent set in $[37]$. This gives the title's equivalent formulation. ## Evidence, assurance and limitations The mathematical bridge is written in the seven-page paper. The package then checks the exact finite objects: all AP edges, counters, indicator equivalences, colouring cuts, two DRAT proofs, explicit satisfying colourings, the small oracle and the replacement neighbourhood. Ordinary and optimized Python modes must agree. Negative controls alter targets, clauses, cuts, hashes, proofs, witnesses, manifests and generated data, and all fifteen are required to fail. The tagged GitHub release and Zenodo record expose the same archive, PDF and checksum sidecar. Public GitHub Actions reconstructs and checks the candidate on a clean runner. These facts establish availability, package integrity and producer-side replay; they do not constitute unaffiliated reconstruction, formal verification of the source-to-CNF theorem, authenticated external specialist review or editorial peer review. The separate 21,329-candidate replacement-neighbourhood calculation is a structural local search, not part of the proof of $v_{2,4}([37])=27$ and not a classification of arbitrary 26-point sets. A targeted literature and GitHub search found no exact prior statement of the bounded equality, but novelty and historical priority remain only partially assessed. ## Who should care and why Ramsey theorists get an exact finite boundary around the classical 27-point construction and a sharply stated remaining global problem. SAT and automated reasoning researchers get a compact proof-carrying benchmark in which semantic translation, CNF proof checking and hostile controls can be audited separately. Researchers studying sparse van der Waerden sets get a reusable normalized search object rather than a numerical hunch about one construction. The release may also be useful as a teaching example: the reason a finite list of colouring cuts can prove a universal exclusion is short, while the scale of the exhaustive search is handled by an independently checkable logical proof. ## Why the problem matters Ordinary van der Waerden numbers ask how long an interval must be before every two-colouring contains an arithmetic progression. The sparse version asks how few carefully chosen integers can force the same phenomenon. That change from interval length to set cardinality creates a difficult global search over both the set and all of its colourings. The equality here resolves the natural interval containing Graham's best-known 27-point construction. It narrows the route to $W^*(4)$: a smaller witness must have primitive diameter greater than 36, while a global lower bound must control all such larger diameters. The theorem does not supply that missing global argument. ## How to inspect or reproduce the result Read the PDF first for the definitions, soundness lemmas and theorem. In the archive, `CLAIMS.json` fixes the claim ceiling, `certificate_N37_k26/` contains the lower CNF, 2,012 colouring cuts and DRAT proof, and `certificate_graham27/` contains the separate upper certificate. Run `./scripts/bootstrap_tools.sh` followed by `./scripts/replay.sh` from the tagged repository. The bootstrap builds the recorded upstream Kissat, CaDiCaL and DRAT-trim commits. Replay reconstructs the formulas before solver calls, checks both proofs, validates the positive colourings, runs the direct oracle, recomputes the structural neighbourhood and exercises all negative controls. The public GitHub Actions run is the clean-checkout reference. `SHA256SUMS` binds the downloadable ZIP and PDF, and the Zenodo DOI archives the same bytes. ## Most valuable next projects 1. Build an unaffiliated source-to-CNF translator and reproduce both certificates in a materially separate software stack. 2. Formalize the exact-cardinality, edge-indicator and colouring-cut soundness lemmas, then connect the checked CNF theorem to a proof assistant. 3. Search for a certified 26-point witness at primitive diameter greater than 36, with canonical affine normalization and symmetry breaking stated before the search. 4. Develop structural reductions that cover whole infinite diameter families, rather than only the declared replacement neighbourhood. 5. Expand the prior-art audit with specialist knowledge of older sparse van der Waerden and Property B computations. ## Paper, archive and package map - **Paper:** the canonical seven-page PDF gives the full finite theorem and source-to-encoding argument. - **Archive:** the ZIP contains both CNFs and DRAT proofs, audited cut data, verifiers, tests, hostile controls, receipts, review records and a complete manifest. - **Repository:** the annotated `v0.1.0-candidate` tag fixes the reviewed source and public replay workflow. - **Zenodo:** version DOI `10.5281/zenodo.22286322` preserves the same ZIP, PDF and checksum sidecar. - **Identity:** the candidate archive SHA-256 is `b1da17612c97f3e932ba06a1e0e93696c6fa05cd5696400dc0ee11d545d8f1d8`. - **Licensing:** original prose, metadata and data are CC0 1.0; original code is MIT; the supplied review is retained as `NOASSERTION` and is not relicensed. ## Open directions for follow-up research - Find a certified 26-point four-term-AP Ramsey set of primitive diameter greater than 36, or prove that none exists at any diameter. - Develop a global structural reduction that covers infinite families of primitive 26-point sets rather than one declared replacement neighbourhood. - Formally verify the source-to-CNF bridge and connect it to machine-checked DRAT or LRAT proof validation. - Independently reimplement the normalized set search, colouring-cut generation and both certificate checks in a materially separate stack. - Determine what, if anything, exact small-k sparse results imply for W(k)-W*(k) or W*(k)/W(k) as k grows. - Obtain an unaffiliated specialist assessment of correctness, closest prior art and historical priority. ## Research process, metrics and reusable methods This is prospective process metadata under the Evidence Press operating model and research-metrics policy. It records the intended handoff, measured scope and claim boundary; it is not evidence that the method accelerated this work. - Work ID: ep-work:ap4-ramsey-diameter-36 - Attempt and metric receipts: ep-attempt:ap4-ramsey-diameter-36-publication-completion: published / partial; scope publication-only; target Publish a reader-first Evidence Press release with provenance-bound fable audio, deterministic art and thumbnail, reciprocal method and work ledgers, green composite CI, guarded zero-cost deployment and exact canonical HTML, paper.json and media readback.; active forecast 70 minutes (35-120); Fermi components Reader-first page, metadata and reciprocal operating records: 1 x 10/20/35 minutes low/central/high (One exact finite result with an unusually important global-versus-finite claim boundary.); Claim-disciplined art, Open Graph image, thumbnail and fable audio: 1 x 10/15/25 minutes low/central/high (One new mathematical slug using established deterministic renderers and the house TTS profile.); Composite build, protocol seals and hosted CI: 1 x 10/20/35 minutes low/central/high (One reader-first release on the current schema with reciprocal work and method records.); Merge, guarded deployment and canonical readback: 1 x 5/15/25 minutes low/central/high (One zero-cost Cloudflare deployment with exact release, media, protocol and preservation checks.); positive-signal/closure probabilities 0.99/0.92 within 120 active minutes; observed active-agent/human/compute/wait/blocked/rework minutes 20/unknown/0/8/0/6; cycles positive/negative/inconclusive 0/0/0; falsification gates 0; architectures tested/rejected 0/0; result target-closed; target reached true; forecast error -50 minutes; ratio 0.29; inside interval false; positive-signal/target-closure Brier scores 0.0001/0.0064; missing telemetry activeHumanMinutes: No instrument captured human direction or review time inside the prospective publication-only boundary.; deduplicatedModelTokens: No active fork-aware task counter exposed exact task-local model-token usage at or after the 18:55:39Z publication boundary, so tokens are not reconstructed from conversation context.; uncachedInputTokens: The runtime does not expose an uncached-input token counter.. Work ledger: https://evidencepress.org/api/work-ledger.json. Metrics policy: https://evidencepress.org/api/research-metrics-policy.json - Intended aims: science - Artifact roles: research-output, evidence-assessment, method-demonstration, communication - Decision object: certificate — A semantically reconstructed SAT and DRAT certificate pair for the exact bounded four-term-AP Ramsey value v_{2,4}([37]) = 27. Scope: Finite subsets of [1,37], equivalently 26-point sets of primitive affine diameter at most 36; not arbitrary primitive diameter, W*(4), the AIM asymptotic questions, independent validation, novelty or priority. - Reusable methods: Certificate-first, proof-carrying research (certificate-first); Structural compression (structural-compression); Adversarial scientific controls (adversarial-controls); Assurance as a vector (assurance-vector); Agent-readable research objects (agent-readable-research-object). Registry: https://evidencepress.org/api/method-registry.json - Targeted clocks: assurance, publication, translation - Semantic bridge: explicit — The paper maps selected-point variables, exact-cardinality counters and progression-indicator equivalences to the finite set problem; proves every full-colouring clause necessary for a Ramsey set; and joins the lower refutation to a separately certified 27-point upper witness, monotonicity and primitive affine normalization. Remaining risks: The source-to-CNF bridge and both certificate pipelines have not been reconstructed by an unaffiliated specialist.; DRAT checking certifies CNF unsatisfiability but does not formally verify the mathematical translation into that CNF.; The 21,329-candidate structural neighbourhood is local and does not control arbitrary larger primitive diameters.; The targeted literature and GitHub search may miss differently phrased, unindexed or unpublished prior work.. - Human judgement gates: Check the exact-cardinality, edge-indicator and colouring-cut soundness lemmas as mathematics rather than inferring the theorem from a green SAT proof.; Keep v_{2,4}([37]) = 27 separate from W*(4) = 27 and from both asymptotic questions in AIM Problem 1.9.; Keep the 21,329-candidate replacement neighbourhood separate from the load-bearing lower certificate and from global structural classification.; Treat public proof checking, internal review and archive availability as distinct from unaffiliated validation, formal verification, peer review, novelty and priority. - Next assurance action: Obtain an authenticated unaffiliated reconstruction of the source-to-CNF bridge and both certificates, then pursue either a certified 26-point witness at larger primitive diameter or a global structural exclusion. - Claim ceiling: An anonymous, AI-assisted, unrefereed computer-assisted finite theorem candidate for v_{2,4}([37]) = 27 with a written soundness bridge, two checked DRAT certificates, hostile controls, public producer replay and internal editorial closure; not W*(4) = 27, an answer to AIM Problem 1.9, independent validation, formal verification, external specialist or editorial peer review, historical priority or demonstrated workflow impact. - Aim-scoped impact evidence: - science: NO_IMPACT_EVIDENCE — Faster or more reliable resolution and assurance of sparse van der Waerden problems in AI-assisted finite search, semantic SAT encoding, adversarial replay, internal review and guarded candidate publication; design none; comparator No matched conventional research, theorem-review or publication workflow was registered.; estimand No effect on discovery time, active human effort, compute, correction rate, proof quality, independent-assurance time, uptake, citation or field outcomes was estimated.; no real-world effect evidence asserted - Parent handoffs: depends-on-claim https://aimath.org/WWN/additivecomb/additivecomb.pdf; inherited claim: AIM Problem 1.9 asks asymptotic questions about the gap and ratio between ordinary and sparse two-colour van der Waerden parameters.; inherited ceiling: The problem source fixes the broader target but does not state or establish this exact bounded equality, its certificate, correctness, novelty or priority.; extends-result https://www.math.ucsd.edu/~ronspubs/83_01_recent_ramsey.pdf; inherited claim: Graham displays the 27-point four-term-AP Ramsey set that supplies this candidate's upper bound.; inherited ceiling: The published construction supplies the witness, not the complete exclusion of every 26-point subset of [37]. ## Verification status Anonymous, AI-assisted, unrefereed computer-assisted finite theorem candidate at internal PASS_WITH_NOTES with no residual or new P0/P1 findings in the final exact-byte confirmation. The finite theorem is a written source-to-encoding argument supported by separately checked lower and upper DRAT certificates. The 21,329-candidate replacement neighbourhood is a non-load-bearing local structural calculation. The unrestricted sparse value W*(4), every primitive diameter above 36, both asymptotic questions in AIM Problem 1.9, independent reconstruction, proof-assistant formalization, external specialist review, journal peer review, exhaustive novelty assessment and priority adjudication remain open or unassessed. ## References 1. American Institute of Mathematics. Open Problems in Additive Combinatorics, Problem 1.9. 2. Graham, R. L. (1983). Recent developments in Ramsey theory. Proceedings of the International Congress of Mathematicians, 1555-1567. 3. Graham, R. L., and Nesetril, J. (1986). Large Minimal Sets Which Force Long Arithmetic Progressions. Journal of Combinatorial Theory, Series A 42(2), 270-276. 4. Hindman, N., and Jordan, J. (2013). On the Size of Minimal Hales-Jewett Sets. Scientiae Mathematicae Japonicae 76(2), 195-207. 5. Dransfield, M. R., Liu, L., Marek, V. W., and Truszczynski, M. (2004). Satisfiability and computing van der Waerden numbers. Electronic Journal of Combinatorics 11. 6. Sinz, C. (2005). Towards an optimal CNF encoding of Boolean cardinality constraints. CP 2005, 827-831. 7. Wetzler, N., Heule, M. J. H., and Hunt, W. A. Jr. (2014). DRAT-trim: Efficient checking and trimming using expressive clausal proofs. SAT 2014, 422-429.