The integer case of the q-analogue of the type D discrete Macdonald-Mehta sum

The sum F_r(n) with the q-weight of the half-integer q-analogue (5.7) of Brent, Krattenthaler and Warnaar (J. Combin. Theory Ser. A 144 (2016), arXiv:1601.06536) for the type D discrete Macdonald-Mehta sum Sr,n(2,1/2,0), taken at integer n, is an explicit product; at q=1, r! F_r(n) = Sr,n(2,1/2,0). It follows from their Okada-type identity (4.6a) together with its image under x_n -> 1/x_n; the combination is neither of the two character sums of their Section 8.4. An independent proof without characters (Pfaffian reduction, semiseparable Gram matrix in a q-Racah basis, double ratio) is formalised in Lean 4 with Mathlib for rational 0<t=q1/2<1 (theorem q_typeD_all, standard axioms only, no sorry); the Lean library and check scripts are included. No claim is made that the factorisation is unknown to experts. An Arabic translation is included.