Monotonicity of Turán determinants for binary Krawtchouk polynomials

Let M, Q ≥ 0 be integers, set D = M + Q, and define ps = [ws](1+w)M(1−w)Q, with ps = 0 outside 0 ≤ s ≤ D. These are the binary Krawtchouk values Ks(Q; D) in the generating-function normalization. We prove that the Turán determinants Tur(s) = ps2 − ps−1ps+1 satisfy Tur(s) ≥ Tur(s+1) for ⌈D/2⌉ ≤ s ≤ D. Consequently, the determinants form a symmetric weakly unimodal sequence and satisfy Tur(s) ≥ 1 for every 0 ≤ s ≤ D. By the dual Jacobi–Trudi identity, they are the rectangular Schur values s(2s)(1M, (−1)Q); for D ≥ 1, this gives positivity and unimodality for a family of general linear character values at involutions. The proof combines a quadratic-form identity with three comparison arguments for the three-term recurrence: a Riccati comparison near the top, a tangent comparison when the smaller exponent is even, and an interval propagation when it is odd. Four polynomial inequalities in the last argument are certified by coefficient positivity; no finite enumeration is needed. All results are formalized in Lean 4 with Mathlib. The formalization, source programs and deterministic replay logs are available at https://github.com/skypher/kraw/releases/tag/v2.0.3. AI-use disclosure. GPT-5.6 Sol assisted with the proof architecture of version 1. Claude Opus 5.5 assisted with the restructured proof and verification code of version 2, and GPT-6 Luna agents wrote most of the Lean formalization under its direction. The author selected and checked the final arguments and is responsible for all mathematical claims, citations, computations, and wording. MSC2020: Primary 33C45; Secondary 05E05, 05E30, 26D05.