Skew-orthogonal proofs, formally verified, of binomial Mehta-type sums at beta = 1

For integers d>=2 and n>=d-1 let V_d(n) = sum over 0<=x_1<...<x_d<=n of prod C(n,x_i) prod_{i<j}(x_j-x_i): the volume of the zonotope generated by C(n,k)(1,k,...,k^{d-1}) and the partition function of the discrete Krawtchouk ensemble (p=1/2) at beta=1. Its product formula, and those of two type B companions, are special cases of the discrete Macdonald-Mehta evaluations of Brent, Krattenthaler and Warnaar (J. Combin. Theory Ser. A 144 (2016), arXiv:1601.06536). We give different proofs by explicit skew-orthogonal polynomials for orthogonal (beta=1) ensembles on the linear lattice, a theory that Forrester and Li (Trans. AMS 2020, arXiv:1902.09042) left open: Krawtchouk polynomials with a Pfaff-Saalschutz triangularisation for V_d(n), Racah polynomials (with Christoffel kernels for even n) for the type B sums, and a rank-one structure for the companion with weight |2x-n|. All three evaluations, for every n and every d, are formalized in Lean 4 with Mathlib without sorry, using only the standard axioms; the Lean library is included. We show that for Re n > d-1 the product formula equals the absolutely convergent infinite sum over 0<=x_1<...<x_d (de Bruijn, Gauss's 2F1(1) and Carlson's theorem; formalized in Lean for every d and every real n>d-1), and that for other n, including the Meixner case n=-N at c=-1, it gives the finite part of the regularized partition function. An Arabic translation is included.