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.

翻译：我们描述了一个可重现的计算框架，用于搜索 $r_3(N)$ 的上界，其中 $r_3(N)$ 是 [1,N] 中不含三项等差序列的最大子集大小。该框架结合了已验证的下界证据、端点迫使、深度 d 证据变量拆分、OEIS A003002 窗口基数剪枝，以及对超时子问题的递归细化。应用于边界情况 N = 212, K = 44 时，该框架在数百万个 CP-SAT 子问题中未发现可行的 44 元素集合，这支持但未证明猜想值 $r_3(212) = 43$。300 秒的 recap 留下 45 个顽固块；一小时的 HiGHS MIP 未能关闭其中任何一个；完整的八小时 HiGHS 审计关闭了 25/45 并留下 20/45 个块的对偶界仍锁定在 0.0。对这些 LP 范式抵抗块的 CDCL/SAT 再攻击通过冲突驱动子句学习关闭了 18 个块；所有这 18 个块均具有独立验证的 DRAT 证明。剩余的两个块 (T1c) 在慷慨的挂钟时间限制下抵抗了所有测试过的范式。我们发布了证据、求解器脚本、结果日志、分层基准实例、已验证的 DRAT/LRAT 证明，以及 T1c 的 Lean 形式证明搜索编码，并将单位间隙问题 $r_3(212) \in \{43,44\}$ 作为更强加性组合界、自定义分支定界或形式证明搜索系统的目标。