Alternating Forms Vanish Beyond Dimension: A Mechanized Proof in Lean 4 with Application to Contact Integrability

Abstract. Any alternating m-linear map on a rank-n module over a commutative ring is identically zero whenever m > n. We give a machine-checked proof of this fact in Lean 4 using two Mathlib lemmas: AlternatingMap. mapₗinearDependent and LinearIndependent. fintypecardₗefinrank. The proof is twelve lines. As a first applicatiAny alternating m-linear map on a rank-n module over a commutative ring is identically zero whenever m > n. We give a machine-checked proof of this fact in Lean 4 using two Mathlib lemmas: AlternatingMap. mapₗinearDependent and LinearIndependent. fintypecardₗefinrank. The proof is twelve lines. As a first application, a pointwise dimension count shows that the Nijenhuis tensor NJ vanishes on the Reeb-orbit direction of the dm3 contact 3-manifold (contact form alpha = dz - r² d-theta). The paper locates this result in a three-level integrability tower and identifies precisely what the deeper levels require. Part of the Principia Orthogona series (ISBN 979-8-9954416-6-3). Series root: 10. 5281/zenodo. 19117399. AXLE repository: github. com/TOTOGT/AXLE. on, a pointwise dimension count shows that the Nijenhuis tensor NJ vanishes on the Reeb-orbit direction Γ of the dm³ contact 3-manifold introduced in Gro26. The paper locates this result in a three-level integrability tower and identifies precisely what the deeper levels require.