Erdős Problem 176 — exact small values of the discrepancy threshold N(k,2) with machine-checkable DRAT certificates (v1.1: N(13,2) = 158)

Exact two-sided values of N(k,2) for k = 2..13 (3, 9, 13, 22, 11, 49, 57, 65, 19, 112, 45, 158) — the least N such that every ±1 coloring of {1,…,N} forces a k-term arithmetic progression with |sum| ≥ 2 (Erdős Problem 176, erdosproblems.com/176). For each k ≤ 12 the bundle ships a DIMACS instance and a DRAT UNSAT proof verified by drat-trim (CaDiCaL 1.7.4 + drat-trim v05.22.2023, containerized and pinned), plus an exact-evaluator-checked witness coloring at N−1: the first publicly available machine-checkable proof objects for these values, independently confirming M. J. Goss, Jr. (2026-06-19, Zenodo 10.5281/zenodo.20763838) for odd k and Spencer (1973) for even k. NEW IN v1.1: N(13,2) = 158, the first published value past k = 12, closed two-sided — an exact-evaluator witness at 157 and a cube-and-conquer UNSAT certificate at 158: 4,096 cubes (complete 2^12 split + color-swap symmetry break, deterministically regenerable from the shipped manifest), every cube's DRAT proof verified by drat-trim (s VERIFIED × 4,096; engines CaDiCaL 1.7.3 and kissat 4.0.4). Also included: one-sided lower bounds for k = 15..25 (evaluator-verified witnesses; N(15,2) ≥ 225, N(23,2) ≥ 508, others in the bundle), the exact integer evaluator, the full audit harness, and the complete ops history. Verification: one-command replay for k ≤ 12 (exit 0, OVERALL PASS); the k = 13 checker wave re-verifies all 4,096 cube proofs in ~6 h. Developed with AI assistance under a machine-verification gate; see README for the production chain and honest labels.