Improving lower bounds for classical two-color Ramsey numbers, specifically strengthening the known increment inequality relating R(k+1,s+1) to R(k,s), and producing a verified new bound for R(12,12).

A constructive proof shows R(k+1,s+1) >= R(k,s) + 2k + 2s for 5 <= k <= s, refining the Xu-Shao-Radziszowski lift via a stronger certificate-orientation lemma and branch-dependent edits of coupled lifts. The construction extracts disjoint red and blue certificates, applies two lifts and two connectors across Type A/Type B and primal/dual orientations. The entire argument is formalized in Lean 4 using Mathlib, covering certificate extraction, the four orientation cases, both lifts, connectors, clique-exclusion arguments, and the final vertex count. Auxiliary Python scripts perform executable construction and enumeration checks that are not premises of the proof.

The inequality is proved and formally verified, giving the new lower bound R(12,12) >= 1641 from R(11,11) >= 1597. The Lean development passes source and axiom audits (only propext, Classical.choice, Quot.sound allowed) with independent kernel replay, and no AI is in the trusted base.