The matchgate even/odd split, kernel-checked: amplitudes are even-dimensional Pfaffians (2×2, 4×4, 6×6, and the recursive general object)

Matchgates are classically simulable because their amplitudes are Pfaffians (signed sums over perfect matchings, equivalently square roots of determinants), and a determinant is a polynomial, computable in polynomial time. This note kernel-checks in Lean 4 + Mathlib the complete even/odd split of that correspondence over the complex numbers: the 2x2, 4x4 and 6x6 Pfaffians square to the determinant (the exact two-, four- and six-qubit amplitudes), the recursive Pfaffian defines the general even-2m object by Laplace expansion along the first row, and any odd-dimensional antisymmetric matrix has determinant 0 (det A = (-1)^n det A, proved structurally). The infrastructure det_fin_four / det_fin_five supplies the general 4x4 and 5x5 determinants Mathlib was missing. The general even-n identity det = Pf^2 (Cayley) and the full matchgate<->free-fermion correspondence remain the open rung, not claimed here. lake build green (9104 jobs), no sorry/axiom/admit.