Witness-split + window-cardinality refinement for $r_3(N)$: Architecture, empirical results, and a structural hard pocket
This work provides a reproducible computational approach and benchmark instances for the open problem of determining r_3(212), targeting additive combinatorialists and formal proof-search systems.
The paper presents a computational framework combining witness-splitting and window-cardinality pruning to search for upper bounds on r_3(N), the maximum size of a 3-term-arithmetic-progression-free subset. Applied to N=212, K=44, the framework found no feasible 44-set across millions of subproblems, supporting the conjecture that r_3(212)=43, but left two resistant chunks unsolved.
We describe a reproducible computational framework for upper-bound searches on r_3(N), the maximum size of a 3-term-arithmetic-progression-free subset of [1,N]. The framework combines a verified lower-bound witness, endpoint forcing, depth-d witness-variable splitting, OEIS A003002 window-cardinality pruning, and recursive refinement of timed-out subproblems. Applied to the frontier case N = 212, K = 44, it found no feasible 44-set across millions of CP-SAT subproblems, supporting but not proving the conjectural value r_3(212) = 43. A 300-second recap leaves 45 resistant chunks; one-hour HiGHS MIP closes none of them; the full eight-hour HiGHS audit closes 25/45 and leaves 20/45 with dual bounds still pinned at 0.0. A CDCL/SAT re-attack on those LP-paradigm-resistant chunks closes 18 via conflict-driven clause learning; all eighteen carry independently verified DRAT proofs. The remaining two chunks (T1c) resist every tested paradigm under generous wall caps. We release the witness, solver scripts, result logs, tiered benchmark instances, verified DRAT/LRAT proofs, and a Lean formal-proof-search encoding of T1c, and frame the unit-gap problem r_3(212) in {43,44} as a target for stronger additive-combinatorial bounds, custom branch-and-bound, or formal proof-search systems.