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

Exact two-sided values of N(k,2) for k = 2..13 and k = 15 (3, 9, 13, 22, 11, 49, 57, 65, 19, 112, 45, 158, 225; N(14,2) = 27 follows from the even-k parity formula and is not certified in this bundle) — 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. v1.1 added N(13,2) = 158, the first published value past k = 12, closed by cube-and-conquer (4,096 drat-trim-verified cube proofs). NEW IN v1.2: N(15,2) = 225, the first published value past k = 13, closed two-sided — an exact-evaluator witness at 224 and a MONOLITHIC UNSAT certificate at 225: a single kissat 4.0.4 run (3 h 16 m) on the seqcounter cardinality instance (190,177 variables, 376,512 clauses), the 3.4 GiB DRAT proof re-checked by drat-trim against the shipped instance (s VERIFIED; instance sha256 recorded in the README). Also included: one-sided lower bounds for k = 17..25 (evaluator-verified witnesses; N(17,2) ≥ 273, 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; the k = 15 check re-runs drat-trim on the shipped proof in ~3 h. Developed with AI assistance under a machine-verification gate; see README for the production chain and honest labels.