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_linearDependent and LinearIndependent.fintype_card_le_finrank. 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^2 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.