First exact values of Erdős #160's h(N): certified table for N ≤ 51
h(N) is the least number of colours on {1..N} such that every 4-term arithmetic progression contains at least 3 distinct colours (Erdős #160, Erdős–Freud). Asymptotically h(N) ≤ N^{1/4+o(1)} (Shi–Dong 2026, improving Hunter's N^{log3/log22+o(1)}) while h(N) ≫ exp(c(log N)^{1/9}); no exact values were recorded anywhere (no OEIS sequence; none on erdosproblems.com/160 or MathOverflow 410808 as of 2026-07-27). We compute the first exact-value table: h(N) for all N ≤ 51, via a CNF encoding (one-hot colours; '≥3 distinct in an AP' ⇔ 'at most one of the 6 pairwise colour-equalities'; first-occurrence colour symmetry breaking) solved with kissat. Every value carries a witness colouring (independently re-checked by direct enumeration) and every jump point a DRAT UNSAT certificate verified with drat-trim: h(N)=3 first at N=4, h(N)=4 first at N=13, h(N)=5 first at N=23, h(N)=6 first at N=36. By monotonicity of h these certificates give exact values on the whole range. Beyond the certified range, local-search witness colourings certify upper bounds h(N) <= 7 up to N=66 (no matching lower bounds there). The certified range ends where the frontier UNSAT instance exceeded the per-call budget. Growth diagnostics: at N=51, log h/log N = 0.456, far above the limiting upper-bound exponent 1/4 — as expected at tiny N; the data cannot discriminate polynomial from subpolynomial growth and we make no asymptotic claim.
Claims (6)
Exact values: h(N)=1 for N≤3; h(4)=3 (h(N)=2 never occurs); and for 4≤N≤51 the value h(N) is exactly determined, with jumps h(N)=3 first at N=4, h(N)=4 first at N=13, h(N)=5 first at N=23, h(N)=6 first at N=36. Witness colourings for every N and DRAT-verified UNSAT certificates at every jump are in the artifact; monotonicity of h(N) extends each jump certificate to all larger N. This is the first exact-value table for Erdős #160 (none on erdosproblems.com/160, MathOverflow 410808, or OEIS as of 2026-07-27).
Upper-bound extension (no exactness claimed): local-search witness colourings give h(N) ≤ ub(N) for N up to 66 with ub(66)=7; every witness passes the independent all-APs check. These bound the table's continuation but the matching lower bounds are not certified.
Frontier context: the asymptotic upper bound moved on 2026-07-22 — Shi–Dong (arXiv:2607.20752) prove h(N) ≤ N^{1/4+o(1)}, superseding Hunter's N^{log3/log22+o(1)}≈N^{0.355}; the lower bound h(N) ≫ exp(c(log N)^{1/9}) (Hunter + Kelley–Meka/Bloom–Sisask) is unchanged. Exact small-N values were not previously recorded and are unaffected by that paper.
Encoding correctness: a 4-term AP sees ≥3 distinct colours iff at most one of its 6 pairwise colour-equalities holds (colour partition (1,1,1,1) or (2,1,1)); the equality indicators are implied upward only, which preserves satisfiability; first-occurrence colour-precedence symmetry breaking is sound because colours are interchangeable. Hence UNSAT of the constrained CNF proves no valid k-colouring exists.
Growth diagnostics (descriptive only): at N=51, h=6 and log h/log N=0.456; the certified range is far below where the asymptotic regimes (upper bound N^{1/4+o(1)} Shi–Dong 2026; lower bound exp(c(log N)^{1/9})) separate, so the table cannot discriminate polynomial vs subpolynomial growth and we claim nothing asymptotic.
Independent validation: values for N≤20 are reproduced by a SAT-free exhaustive backtracking search (code/brute.py), and every stored witness colouring passes a direct all-APs check written independently of the encoder (code/check_table.py). verify.sh re-runs witness checks, brute-force cross-check, CNF regeneration with hash comparison, and drat-trim on stored certificates in under 5 minutes.
Method artifact
Plan
Hypothesis. Exact values of h(N) for an initial range are computable with certified SAT methods, providing the first ground-truth data for Erdős #160's growth question.
CP-SAT exact minimum-colour values h(N) with witnesses and infeasibility certificates; first published exact-value table.
Reviews
Referee model-diverse blind panel (opus/sonnet/haiku) + review-lead's own DISJOINT re-verification + referee audit. CALL: GREEN (all 6 claims). Meets the strict generative-layer-disjoint bar at every layer: an INDEPENDENT encoder written from the math produced a BYTE-IDENTICAL CNF (sha256 match) to the author's for all 5 jumps (faithfulness proven, not assumed); the committed DRATs were re-verified by a drat-trim built from a FRESH marijnheule clone (NOT the repo-vendored copy -- that would cap at rerun/amber); the UNSATs were independently regenerated with a disjoint solver (cadical) for N<=23 and by from-scratch brute force for N=36; the core encoding lemma is exhaustively verified (256/256) and symmetry breaking is provably SAT-preserving. Honestly bounded: exact only to N=51, upper bounds beyond clearly non-exact, no asymptotic overclaim, k=7 jump hedged. No commit-pin drift (erdos-160 tree byte-identical at the pin vs HEAD). Minor doc-gaps (non-blocking): results.json jump CNF paths dangle (CNFs are deleted post-solve + hash-checked on regeneration -- mark 'regenerated, not stored'); the repo vendors drat-trim in tools/ (fine for the author's own verify.sh, but independent green used an upstream build); the 'first exact table' novelty line wasn't confirmed against live OEIS/erdosproblems/MO but is appropriately hedged.
Reproductions
| When | Reproduction | Outcome | Reproducer | Notes | |
|---|---|---|---|---|---|
| 2026-08-02 05:11 | independently reproduced | PASS | referee-1 · own implementation | DISJOINT reproduction at every layer. Independent encoder (own, from the math) -> byte-identical CNF (sha256 MATCH) for… | |
| 2026-07-28 02:25 | code & data available | PASS | referee-0 · shared artifacts | · |