Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0

Technische Samenvatting: Stokessetheorema voor Gladde Singuliere Kubussen in Lean 4

Probleemstelling
Per april 2026 ontbrak er in het Lean 4-ecosysteem (specifiek mathlib4) een volledige formalisering van het Stokessetheorema voor differentiaalvormen op gladde variëteiten met rand of voor singuliere ketens. Hoewel mathlib4 beschikte over de divergentiestelling voor as-georiënteerde dozen en een abstracte uitwendige afgeleide (extDeriv), bood het nog geen stelling die de pullback van een differentiaalvorm integreert over een gladde singuliere kubus (een gladde afbeelding van een eenheidskubus naar een willekeurige Euclidische ruimte) en deze gelijkstelt aan het alternerende som van integralen over de randvlakken. Bestaande formalisaties, zoals het werk van Harrison in HOL Light, bestreekten convexe en polyedrische domeinen, maar behandelden geen gladde singuliere parametriseringen of de specifieke infrastructuur van mathlib4's abstracte uitwendige algebra.

Methodologie
De auteurs presenteren een "sorry-vrije" formalisering (nul onbewezen aannames) die de kloof overbrugt tussen coördinaatgebaseerde integratie en abstracte differentiaalmeetkunde. De ontwikkeling rust op drie methodologische pijlers:

1. Echte Pullback via Fréchet-afgeleide: De kernconstructie definieert de pullback van een differentiaalvorm $\sigma^*\omega$ met behulp van de Fréchet-afgeleide ($fderiv$) van een globaal $C^\infty$-afbeelding $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$. In tegenstelling tot eenvoudige pre-samenstelling van coëfficiënten, past deze definitie de vorm toe op het beeldpunt $\sigma(x)$ op vectoren die vooruitgeschoven zijn door $D\sigma(x)$, conform de standaarddefinities uit de differentiaalmeetkunde.
2. Reductie tot Box-Stokes: De bewijsstrategie reduceert het singuliere geval tot het geval van as-georiënteerde dozen. Door gebruik te maken van de extDeriv_pullback-stelling van mathlib4, stellen de auteurs de naturaliteitsidentiteit $d(\sigma^*\omega) = \sigma^*(d\omega)$ vast. Dit maakt het toepassen van de bestaande box-Stokessstelling (afgeleid van de divergentiestelling van mathlib4) mogelijk op de getrokken vorm $\sigma^*\omega$ over het parametervlak $[0,1]^{n+1}$.
3. Vlakkenmatching en Algebra op Ketenniveau: Een kritisch technisch onderdeel is de "vlakkenmatching-identiteit", die bewijst dat de integraal van de getrokken vorm over een randvlak van een doos exact overeenkomt met de integraal van de vorm over het overeenkomstige singuliere vlak. Bovendien formaliseren de auteurs de ketencomplex-identiteit $\partial(\partial\sigma) = 0$ voor singuliere ketens. Dit wordt bereikt niet door een randhomomorfisme te definiëren op ongedecoreerde dozen, maar door een tekenomkerende, vastpuntvrije involutie te construeren op de indexset van dubbele randen, waarbij wordt bewezen dat gepaarde termen algebraïsch elkaar opheffen.

Belangrijkste Bijdragen
Het paper levert een uitgebreide formalisering die 44 Lean-modules omvat (ongeveer 4.000 regels) met 205 benoemde declaraties. De specifieke bijdragen zijn:

• Singuliere Stokessstelling: Een stelling die stelt dat voor elke globaal $C^\infty$-afbeelding $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ en elke $C^\infty$ $n$-vorm $\omega$, de integraal van $\sigma^*(d\omega)$ over de eenheidskubus gelijk is aan het alternerende som van integralen van $\sigma^*\omega$ over de $2(n+1)$ vlakken.
• Brugstelling: Een formeel bewijs dat valideert dat de coördinaatgebaseerde uitwendige afgeleide van de auteurs (extDerivCoord) consistent is met de abstracte extDeriv van mathlib4 wanneer deze wordt geëvalueerd op standaardbasisvectoren. Dit waarborgt dat de coördinaatimplementatie wiskundig correct is ten opzichte van de abstracte API van de bibliotheek.
• Extensies op Ketenniveau: De uitbreiding van het Stokessetheorema tot formele $\mathbb{Z}$-lineaire combinaties van singuliere kubussen (singuliere ketens) via lineariteit.
• Bewijs van $\partial^2 = 0$: Een formeel bewijs van de ketencomplex-identiteit $\partial(\partial\sigma) = 0$ voor singuliere ketens, waarbij gebruik wordt gemaakt van een combinatorische involutie op de indexset van dubbele vlakken.
• Dimensionale Specialisaties: Directe instantiaties van de hoofdstelling die het Fundamentele Stelling van de Calculus (FTC), de Stelling van Green, de Divergentiestelling en de 3D-stelling van Gauss terugwinnen, evenals partiële integratie en de Leibniz-regel.
• Axioma-audit: Verificatie dat de gehele ontwikkeling uitsluitend afhankelijk is van de drie standaard Lean 4-axioma's (propext, Classical.choice, Quot.sound), bevestigd via 79 systematische #print axioms-controles.

Resultaten en Reikwijdte
De formalisering bewijst het Stokessetheorema succesvol voor:

1. Gladde Singuliere Kubussen: Afbeeldingen $\sigma$ die globaal glad zijn op $\mathbb{R}^{n+1}$, geïntegreerd over het parametervlak $[0,1]^{n+1}$.
2. As-georiënteerde Dozen: Coördinaat $n$-vormen op dozen $[a,b] \subset \mathbb{R}^{n+1}$.

Het paper noteert expliciet de volgende beperkingen en grenzen van de reikwijdte:

• Geen Variëteitentheorie: Het integratiedomein is strikt het parametervlak of een doos. Het werk formaliseert geen integratie over algemene gladde variëteiten, noch gebruikt het partitions of unity, kaarten of atlas.
• Globale Gladheid: De singuliere afbeeldingen moeten $C^\infty$ zijn op het gehele $\mathbb{R}^{n+1}$, een sterkere voorwaarde dan gladheid op de gesloten kubus alleen. Deze keuze is gemaakt om de formalisering te vereenvoudigen door randregulariteitsargumenten te vermijden en ervoor te zorgen dat de Fréchet-afgeleide overal goed gedefinieerd is.
• Geen Semantiek van Beelddomein: De stelling behandelt de integraal als een bewerking over het parametervlak. Het bewijst niet dat het beeld van $\sigma$ een deelvariëteit of een georiënteerde geometrische keten in de doelruimte vormt.

Betekenis en Claims
De auteurs claimen dat dit werk de eerste volledige Lean 4-formalisatie van het Stokessetheorema voor gladde singuliere kubussen biedt met een "echte" pullback van differentiaalvormen. De betekenis hiervan ligt in:

1. Overbruggen van Concreet en Abstract: Het "brugstelling"-patroon valideert een concrete coördinaatimplementatie tegen de abstracte uitwendige afgeleide van mathlib4, en biedt een herbruikbare methodologie voor toekomstige formalisaties.
2. Hergebruik van Infrastructuur: De ontwikkeling maakt zwaar gebruik van bestaande mathlib4-infrastructuur (divergentiestelling, extDeriv_pullback), en demonstreert hoe hoogwaardige bibliotheekcomponenten kunnen worden samengesteld om complexe meetkundige stellingen te bewijzen zonder fundamentele analyse opnieuw te moeten uitvinden.
3. Complementariteit: Het werk is complementair aan de HOL Light-formalisatie van Harrison. Waar Harrison convexe/polyedrische domeinen behandelt met gauge-integratie, behandelt dit werk gladde singuliere parametriseringen met Bochner-integratie en de differentiaalmeetkunde-API van mathlib4.
4. Fundamentele Klaarheid: Door $\partial^2=0$ te bewijzen en het Stokessetheorema op ketenniveau vast te stellen, bieden de auteurs een noodzakelijk lokaal bouwsteen voor een toekomstige volledige formalisering van het Stokessetheorema op gladde variëteiten met rand, zodra de manifold-integratie- en oriëntatie-API's van mathlib4 rijper zijn.

Het paper concludeert dat hoewel het de problemen van integratie op algemene variëteiten niet oplost, het wel de kritieke "kubische-keten"-laag met echte pullbacks vestigt, dienend als een geverifieerde fundering voor toekomstige uitbreidingen.