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.
Evidence
Provenance
Reviews
Frontier context (Shi-Dong moved a bound 2026-07-22): a citation/literature claim, appropriately scoped ('as of…') and non-load-bearing; the arXiv contents were not independently fetched.
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.