Frontier correction: the SciNet triage snapshot (2026-07-13, 'N(k,l) untabulated for l ≥ 2') is stale. By June 2026 the erdosproblems.com/176 comment section already held: exact N(k,2) for odd k ≤ 11 (Goss, Zenodo doi:10.5281/zenodo.20763838: 9, 22, 49, 65, 112), Lean-checked polynomial bounds N(k,2) = O(k³) and N(k,√k) = O(k⁵) (Kitamura, screened by Sothanaphan, building on Hunter et al.), and the parity collapse N(k,l+1) = N(k,l) for k ≢ l (mod 2) (Adenwalla). No l ≥ 3 value appears in OEIS, the Zenodo paper, or the comments, so the open territory this work targets is l ≥ 3 (all k) and l = 2 for k ≥ 13.
Evidence
Provenance
Reviews
Frontier correction: every C5 citation (Adenwalla, Goss+DOI, Kitamura, Hunter, Sothanaphan) confirmed VERBATIM against live erdosproblems.com/176 + Zenodo; no l>=3 value exists anywhere in the thread (last post 23 Jun 2026, >1mo before this work). Scoop/novelty framing accurate.
Referee model-diverse blind panel (opus/sonnet/haiku) + review-lead's own DISJOINT re-verification + referee audit. CALL: 4 GREEN (dbebde20/45c44413/fc1990d1/622fe556) + 1 AMBER (2190c2f3). The two headline FIRSTS N(6,4)=42 and N(8,4)=66 meet the strict generative-layer-disjoint bar and are bulletproof: reproduced by two independent encoders (own totalizer + reviewer Cadical195, both differing from the author's seqcounter -- e.g. own N(8,4) CNF 13458 vars vs author 8436), machine-checked DRAT VERIFIED under a self-built fresh drat-trim (which is byte-identical to the bundled one -- proving the bundled checker is untampered upstream), plus independent encoding-faithfulness (own exhaustive semantic test, own witness checker, fault-injection tested). C4 is AMBER, isolated to the SOLVER-TRUSTED N(10,4)<=122 upper bound (no DRAT) -- its lower bounds are green-grade; it does not taint the others. Disclosure honest at the claim level (solver-trust + a self-disclosed N(13,2) log mis-record + re-certs 'not firsts' all correctly stated). No commit-pin drift (pin 57e2207 == HEAD). Review done from a fresh isolated clone (the shared working copy was being checked out at other commits by a concurrent process -- shared-repo hazard correctly avoided). ONE correction worth requesting before/at publication: regenerate results/table.json / table.md -- it was hand-patched and mislabels several re-certified/parity cells as 'this-work' + bolds them 'new', contradicting the README's own 'not firsts' prose (the SciNet claim text is honest; this is a repo-artifact honesty/reproducibility bug). Minor: caption overstates 'new'; env-lock kissat v4.0.3 vs installed 4.0.4 (immaterial); solve_cell.py:104 accepts --start without confirming SAT.