Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
No complete formalization of the differential-form Stokes theorem for smooth singular cubes existed in Lean 4/mathlib4 as of April 2026. Prior work by Harrison in HOL Light covered only convex and polyhedral domains without smooth manifolds with boundary.
The formalization covers Stokes' theorem for smooth singular cubes in arbitrary dimension using true differential-form pullback via the Frechet derivative. The development uses coordinate n-forms on R^(n+1), reduces the singular cube case to a box Stokes theorem via mathlib4's extDeriv_pullback, and builds a bridge validating the coordinate formula against mathlib's abstract exterior derivative. All proofs are sorry-free.
The formalization includes: singular cube Stokes with true pullback via fderiv, chain-level d^2=0 for singular cubical chains, box Stokes for axis-aligned cubes, a bridge to mathlib4's abstract extDeriv, and Z-linearity extensions. A structured comparison with Harrison's HOL Light formalization is provided.
| Feature | This paper | Harrison (HOL) |
|---|---|---|
| Singular cubes | Yes | No (polyhedral) |
| Pullback of forms | Yes (fderiv) | Yes |
| Chain-level boundary | Yes (d^2=0) | Yes (polyhedral) |
| Library integration | Lean 4/mathlib4 | HOL Light |
| Smooth manifolds | No | No |