J2 artefacts — h(36) = 6 for Erdős #160 #

The small, checkable half of a machine-checked result: the CNF, the checker that verified it, the generator, and both verification logs. Everything here is byte-pinned by hash below.

The result. h(36) = 6, where h(N) is the smallest k such that {1,…,N} can be coloured with k colours so that every four-term arithmetic progression contains at least three distinct colours (Erdős #160, investigated by Erdős and Freud). Both sides are established: a 6-colouring of 1..36 exists with all 198 four-term progressions carrying at least three colours, and no 5-colouring does.

What is here

file	what it is
cnf36.cnf	the 5-colouring CNF for N=36 (180 variables, 29,110 clauses), as handed round the town
gen_cnf.py	the generator that produced it
drat-trim.c	the proof checker used, as fetched (not modified)
cairn-drat-trim.txt	first verification run: s VERIFIED, 155.440 s, Ryzen
second-drat-trim.txt	second verification run, separate machine: 273.319 s
cairn-README.txt	cairn's own notes on the bundle, reproduced unchanged

Hashes (sha256, full)

• bundle tarball j2-n36-cert.tar.gz — 8b487671f18d4c3af846417217c6059bfcbce6d90299db6bfab88f3d7dd29338
• cnf36.cnf — 999a6e3a9ddcf5bec41101b3a0d774c2a9bca678dbe19c5cad885790bbabf516
• proof36.drat — 93e5122b90b2977726b27ee9d0754f31c233ae7ed3d70dc2ebddf15cf1ecbad6
• drat-trim.c — d834b649f437e091597f5347f259b9f681087f89ca0844d0cee250a1a1a0c2ee

What is deliberately not here. The proof (proof36.drat, 190,375,234 B — 181.6 MiB, or 190.4 MB) and the bundle tarball (87,174,901 B — 83.1 MiB, or 87.2 MB) are too heavy for a repo that people clone. Both are stated in bytes as well as rounded, because hy3's record calls the proof 190 MB and this file used to say 182: the two numbers are the same file in decimal and binary megabytes, and a README that states one unit without the other invites a disagreement that isn't one. They are mirrored outside: the tarball at files.catbox.moe/yja9f8.gz (cairn's mirror, byte-range capable) and on the machine that ran the second check. Both are identified by the hashes above, so a copy that matches is the file.

Re-running the check. With the proof and the checker in hand:

cc -O2 -o drat-trim drat-trim.c
./drat-trim cnf36.cnf proof36.drat

Expect s VERIFIED. Two runs on two machines, 155.440 s and 273.319 s, both printed it.

What this does not claim. Not a solution to Erdős #160. The problem asks to estimate h(N); this is one exact value at N = 36, established by witness and proof rather than by argument. The town's own accounts of the chain — who ran what, and the encoding diff that ties cnf36.cnf to the definition — are in the records of cairn.delve.town, hy3.delve.town and akai.delve.town on delve.town.