Zarankiewicz numbers z(m,n;3,4): SAT witnesses and DRAT-certified exact values (OEIS A006615 and A006625)

Witness matrices and machine-checked certificates for Zarankiewicz numbers z(m,n;3,4) in the oriented convention (forbidden: 3-row × 4-column all-ones submatrices), supporting OEIS A006615 (a(n) = z(n,n;3,4)+1) and A006625 (a(n) = z(n,n+2;3,4)+1). This is Zarankiewicz's problem (1951); Erdős problem #713 supplies related asymptotic bipartite Turán context. Version 1 incorrectly cited #712, which concerns a different hypergraph Turán problem. Certified exact values (v2): z(12,12;3,4) = 90 (A006615 a(12) = 91, a new term) and z(11,13;3,4) = 89 (A006625 a(11) = 90, also a new term; the published sequence previously ended at a(10) = 79). Certification partitions on the first row's one-count under double-lex symmetry breaking: every case is refuted by kissat, every retained proof is verified by drat-trim, and the exhaustiveness of each split is itself DRAT-certified. The package includes the full certificate structure, proof hashes, append-only evidence and independent witness-verification tools. Lower-bound witnesses: matrices for z(n,n;3,4), n = 13..21, and for z(12,14;3,4) and z(13,15;3,4). All 13 packaged witnesses were re-verified during the v2 build. Related work: Jeremy Tan, arXiv:2203.02283, introduced SAT and symmetry-breaking methods for square forbidden minors. Alexander Towell, DOI 10.5281/zenodo.19985042, published SAT partition decompositions for other z(m,n;3,4) values. The present exact terms, lex-prefix formulation and mechanically certified nested case covers are distinct contributions. Search, encodings and the certification pipeline were developed in close collaboration with an AI assistant (Claude, Anthropic). Witnesses through n = 16 were independently checked by Alex Towell (private communication, 2026-08-03): witnesses only, not the proof pipeline.