Zusammenfassung. Jede wechselnde m-lineare Abbildung auf einem Rang-n-Modul über einem kommutativen Ring ist identisch null, wann immer m > n. Wir geben einen maschinenüberprüften Beweis für diese Tatsache in Lean 4 unter Verwendung von zwei Mathlib-Lemma: AlternatingMap.mapₗinearDependent und LinearIndependent.fintypecardₗefinrank. Der Beweis umfasst zwölf Zeilen. Als erste Anwendung zeigt eine punktweise Dimensionszählung, dass der Nijenhuis-Tensor NJ in der Reeb-Orbit-Richtung der dm³-Kontakt 3-Mannigfaltigkeit verschwindet (Kontaktform alpha = dz - r² d-theta). Das Papier lokalisiert dieses Ergebnis in einem Integrabilitätsturm mit drei Ebenen und identifiziert präzise, was die tieferen Ebenen erfordern. Teil der Principia Orthogona-Serie (ISBN 979-8-9954416-6-3). Serienwurzel: 10.5281/zenodo.19117399. AXLE-Repository: github.com/TOTOGT/AXLE.
Pablo Nogueira Grossi (Tue,) hat diese Frage untersucht.