A kernel-verified universal theorem on reduced representatives of quadratic APN permutations

We report a Lean 4 formalization, with mathlib, of a theorem on quadratic almost perfect nonlinear (APN) permutations: for every odd n ≥ 9 and every quadratic APN permutation Q of F2n there are invertible F2-linear maps L, A such that the formal derivative of the reduced (degree < 2n) polynomial representative of L∘Q∘A has no zero and is exactly two-to-one. Quadratic APN functions are classified only in small dimensions, and the proof does not use a classification; the formal proof treats all odd n ≥ 9 and all equivalence classes uniformly and depends only on the axioms propext, Classical.choice and Quot.sound. The proof is an existence argument by counting: a fixed-input construction reduces the problem to the choice of one input, an encoding of F2-linear maps by vectors of F2nn turns that choice into linear algebra over F2n, a cofactor vector is obtained as a polynomial by dividing an adjugate by a prime variable, and a comparison of binary matrices by rank, closed by the Schwartz–Zippel bound, produces a good input uniformly in n. We describe two parts of the development as reusable patterns. The polynomial cofactor is also proved, outside the APN setting, for every n×n matrix of polynomials with n ≥ 2 whose left kernel contains the generic vector, and applied to the cross-product matrix. The counting skeleton turns projective injectivity into a cardinality bound without quotient types. We list the general lemmas the development had to supply and state what the kernel check covers and what it does not. Files. manuscript.pdf is the paper. apnlift-formalization-paper-1.0.0.zip is the archive of release v1.0.0 of https://github.com/hirokifukui/apnlift-formalization-paper: manuscript sources, the Lean excerpts printed in the paper with their manifest and extraction script, and a small Lean project for Section 4.1 that imports apnlift v1.0.4 unchanged, with its verification record. The Lean development of the main theorem is apnlift v1.0.4 (10.5281/zenodo.23058755). Licences. Text (manuscript, README, CITATION.cff): CC BY 4.0. Lean code, script and excerpts: MIT. See LICENSE in the archive. Prepared for submission to the Annals of Formalized Mathematics.