Certified even-case values for the Frankl/Balogh–Linz–Patkós t-intersecting k-Sperner conjecture: (9,3,2)=120 and (9,3,3)=129, with DRAT certificates

Machine-checkable certificates fixing the exact maximum size of small t-intersecting, k-Sperner families in the Boolean lattice 2^[n], in the even-parity case (n+t even) — Frankl Conjecture 1.6 (Eur. J. Combin. 93 (2021) 103279) = Balogh–Linz–Patkós Conjecture 1.7 (arXiv:2209.01656) = Yang–Zhang Conjecture 1.4 (arXiv:2607.03026). Certified both directions: maximum at (9,3,2) is exactly 120 and at (9,3,3) exactly 129, each via a kissat-generated DRAT proof checked by drat-trim (exit code 0) for the upper bound, and an explicit witness family verified by independent exact-arithmetic code for the lower bound. Both equal the conjectured values. To the best of our determination as of 2026-07-09 these are first settlements; both cells fall outside the ranges of Frankl's Theorems 1.11 and 4.1, with (9,3,2) the smallest even-parity instance not covered by Theorem 1.11. Cross-checked against Yang–Zhang's refutation of the odd-parity case at the same (t,k). Produced with substantial AI assistance (Anthropic's Claude); see AI_DISCLOSURE.md. Reproduction instructions and SHA256 checksums included.