Machine-checked proof archive: Haugland's 2131-vertex Moser-spindle-free unit-distance graph is 5-chromatic (cube-and-conquer certificate for the pair property of G1)

This record contains the complete machine-verifiable proof archive (28 GB uncompressed, 2 gzip volumes of 7.9 GB) for the theorem of J. K. Haugland (arXiv:2608.04542 v4) that his 2131-vertex Moser-spindle-free unit-distance graph G3 has chromatic number 5. The graph was reconstructed from the paper's definitions in exact cyclotomic arithmetic (ℚ(ζ₈₄) and ℚ(ζ₄₂₀); every intermediate count matches the paper), and the following statements were certified by machine: the edge list is the complete unit-distance graph on the 2131 exact points; G3 contains no Moser spindle as a subgraph (exact enumeration and a drat-trim-checked UNSAT certificate); G3 has a 5-colouring (checked edge by edge); and G3 has no 4-colouring. The last statement follows the paper's decomposition: (L1) in every 4-colouring of the 740-vertex graph G1 the points (0,0) and (0,√3) receive different colours; (L2) four isometric copies of G1 lie in G3 (exact arithmetic); (L3) the four resulting constraints plus the 4-colouring clauses of G3 are unsatisfiable (drat-trim-checked DRAT proof). Plain CDCL could not settle L1 (22 solver/encoding runs of 30 minutes all timed out), so L1 is certified by cube-and-conquer: march_cu (static depth 14) splits the CNF into 14 786 cubes; every cube is refuted by kissat 4.0.4 (mean 0.46 s, max 8.6 s) and each of the 14 786 DRAT proofs, lifted to the plain encoding, is checked by drat-trim (a 5 % sample also by the formally verified checker cake_lpr); the cover (the conjunction of the negated cubes) is itself a drat-trim-checked refutation. The archive contains the exact coordinate files, all CNFs, the cube file, the cover certificate, all 14 786 leaf proofs, the L2/L3 certificates, the spindle-freeness certificate, the 5-colouring, the scripts that produced everything, sha256 fingerprints of every file and of the tool binaries, and a one-command re-verification script (`bash rerun.sh`, about 12 minutes on 14 cores). The small companion repository (README, inputs, cubes, cover, L2/L3 certificates, scripts) is the GitHub layer of the same release and pins this archive by sha256. Computations were orchestrated with Claude Code (Anthropic); all mathematical claims are independently machine-checked by drat-trim / cake_lpr and reproducible from the included scripts.