MSC 2020: 58A10 (Differential forms), 68V20 (Formalization of mathematics).
Keywords: Stokes’ theorem, formal proof, Lean 4, mathlib, differential forms, singular cubes, exterior derivative, pullback.

0.0.0.1 What this paper proves, briefly.

For any globally \(C^\infty\) map \(\sigma : \mathbb{R}^{n+1} \to \mathbb{R}^m\) and any \(C^\infty\) \(n\)-form \(\omega\) on \(\mathbb{R}^m\), integrating the pullback of \(\mathrm{d}\omega\) over the unit cube equals the alternating sum of pullback integrals over the \(2(n{+}1)\) faces—formalized in Lean 4 with zero sorry and only the standard foundational axioms. The precise scope and limitations, including the relationship to manifold Stokes, are discussed in 13.

1 Introduction↩︎

The generalized Stokes’ theorem [2], [3] is one of the central results in differential geometry, unifying the fundamental theorem of calculus, Green’s theorem, the classical divergence theorem, and the curl theorem into a single statement: for an oriented smooth manifold \(M\) with boundary and a differential form \(\omega\) of appropriate degree, \[\label{eq:stokes} \int_M \mathrm{d}\omega = \int_{\partial M} \omega\tag{1}\] Prior to this work, to our knowledge no complete formalization of the differential-form Stokes theorem (for smooth manifolds with boundary, singular chains, or comparable generality) exists in Lean 4 [4]/mathlib4 [5], [6] as of April 2026. Harrison [1] formalized Stokes’ theorem in HOL Light for convex and polyhedral domains, building on the Euclidean space foundations of [7]. Harrison’s published development does not cover smooth manifolds with boundary (see 13.3 for a detailed comparison).

In this paper, we present a sorry-free Lean 4 formalization of Stokes’ theorem at two levels:

1. Smooth singular cubes: For any \(C^\infty\) map \(\sigma : \mathbb{R}^{n+1} \to \mathbb{R}^m\) and smooth \(n\)-form \(\omega\) on \(\mathbb{R}^m\), the integral of the pullback \(\sigma^*(\mathrm{d}\omega)\) over the unit cube equals the oriented sum of face integrals of \(\sigma^*\omega\). The pullback is the true differential-form pullback, using the Fréchet derivative of \(\sigma\).

2. Axis-aligned boxes: For any \(C^\infty\) coordinate \(n\)-form on \(\mathbb{R}^{n+1}\) and any box \([a, b]\), the integral of \(\mathrm{d}\omega\) (evaluated on the standard frame) equals the boundary integral.

The singular cube theorem (singularStokes) allows smooth maps \(\sigma : \mathbb{R}^{n+1} \to \mathbb{R}^m\) that can parametrize curves, surfaces, and higher-dimensional objects (possibly degenerate or self-overlapping), with integration always over the parameter cube—broader as a parametrized-chain statement than axis-aligned boxes alone, though still short of smooth manifolds with boundary or image-domain theory.

1.1 Contributions↩︎

Our central contribution is the singular-cube theorem; the box, bridge, and chain results form the technical infrastructure that makes the singular case go through.

1.1.0.1 Headline contributions.

1. Stokes for smooth singular cubes with true pullback via fderiv (2). The proof reduces to box Stokes via mathlib4’s extDeriv_pullback, which gives \(\mathrm{d}(\sigma^*\omega) = \sigma^*(\mathrm{d}\omega)\), and a chain-rule face-matching identity (3) that we formalize.

2. Chain-level \(\partial^2{=}0\) for singular cubical chains, proved via a sign-reversing fixed-point-free involution on the double-boundary index set (23); chain-level Stokes is also formalized by extending the singular theorem \(\mathbb{Z}\)-linearly over Finsupp.

3. A formal bridge from our coordinate representation to mathlib4’s abstract extDeriv (5), proving that our coordinate formula is the evaluation of the abstract exterior derivative on standard basis vectors, and a unified statement (stokes_extDeriv_smooth) that needs only one ContDiff hypothesis.

1.1.0.2 Supporting infrastructure.

1. A sorry-free proof of box Stokes for axis-aligned cubes in arbitrary dimension \(n+1\) (4), reducing to mathlib4’s divergence theorem [8] via a signed-coefficient construction (short proof body; the work is in the definitions).

2. Box chain infrastructure: \(\mathbb{Z}\)-linear combinations of boxes with Stokes extended by linearity, two-box additivity, and shared-face cancellation (7).

3. Box-level \(\partial^2{=}0\) sign and face cancellation: for each codimension-2 face, the two boundary paths produce the same face box with opposite signs—proved without defining \(\partial\) as a chain homomorphism on undecorated boxes.

4. Dimensional specializations: FTC (\(n{=}0\)), rectangular Green’s theorem (\(n{=}1\), with four-edge decomposition), divergence consistency, and 3D Gauss; plus calculus corollaries (integration by parts, Leibniz product rule). All are direct instantiations of stokes_smooth, not independent derivations.

5. A 1D agreement check (6.1) showing that the Stokes-derived FTC equals mathlib4’s interval-integral FTC.

6. A structured comparison with Harrison’s HOL Light Stokes for convex/polyhedral domains (13.3), and an honest assessment of what remains for full manifold Stokes (13).

1.1.0.3 Theorem dependency transparency.

stokes_on_box is a direct wrapper around mathlib4’s divergence theorem (the mathematical content is the signed-coefficient construction). stokes_smooth derives hypotheses from \(C^\infty\) and calls stokes_on_box. singularStokes reduces to stokes_smooth via extDeriv_pullback and the face-matching identity. stokes_singular_boundary restates singularStokes with the boundary integral on the left; stokes_singular_chain is the corresponding formal-chain version using singularBoundarySingle. stokes_chain extends by \(\mathbb{Z}\)-linearity (Finsupp.induction for singular chains, Finsupp.sum_congr for box chains). The FTC, Green, divergence, and Gauss results are dimensional instantiations of stokes_smooth. dd_zero_abstract is a direct invocation of mathlib4’s extDeriv_extDeriv. bdry_sq_sign_cancel is independent sign arithmetic (no analysis dependency; uses only omega and ring lemmas).

1.2 Relation to Existing Work↩︎

1.2.0.1 Harrison’s HOL Light formalization.

Harrison [1] formalized a version of Stokes’ theorem in HOL Light for convex and polyhedral domains in \(\mathbb{R}^N\), extended to polyhedral chains. Contrary to what some summaries suggest, Harrison’s formalization does not cover arbitrary smooth manifolds with boundary; it operates on convex polytopes with the Henstock–Kurzweil gauge integral. With our singular cube extension, the mathematical scope of the two developments is complementary but different: Harrison proves Stokes for convex/polyhedral domains in \(\mathbb{R}^n\) extended to polyhedral chains, while our work uses smooth singular cubical parametrizations from the unit cube. The key infrastructure differences remain: (1) Harrison works in HOL’s simple type theory; we use Lean 4’s dependent types; (2) Harrison builds all integration from scratch; we reduce to mathlib4’s divergence theorem; (3) we provide a bridge to mathlib4’s abstract extDeriv and use extDeriv_pullback for the singular theorem; we are not aware of a directly comparable bridge to an independently developed abstract exterior-derivative API in HOL Light, since HOL Light does not maintain such an independent abstract exterior algebra alongside its integration theory. A detailed structural comparison appears in 13.3.

1.2.0.2 Mathlib infrastructure.

As of the mathlib4 version pinned in this project (April 2026), the library provides:

• The box divergence theorem (integral_divergence_of_hasFDerivAt_off_countable'), which uses the Bochner set integral despite its historical connection with Henstock–Kurzweil-style divergence theorems [8]. Our box Stokes is a direct wrapper around this result.

• The abstract exterior derivative (extDeriv) for differential forms [9]

• Naturality of pullback (extDeriv_pullback) [9]

• Continuous alternating maps (ContinuousAlternatingMap)

• Smooth manifold infrastructure (SmoothManifoldWithCorners) [10]

However, mathlib4 does not yet provide: integration of differential forms on manifolds, orientation theory for manifolds with boundary, or a differential-form Stokes theorem comparable to the present statement (though it does provide the box divergence theorem from which our box Stokes reduces). Our work provides the first Lean 4 formalization of Stokes’ theorem for smooth singular cubes, contributing to the growing body of Lean 4 formalizations reported in venues such as AFM [11] and ITP [12].

1.2.0.3 Broader ITP landscape.

Beyond Harrison’s HOL Light work, integration and measure theory have been formalized extensively in Isabelle/HOL by Hölzl, Immler, and others [13], providing foundational infrastructure for Lebesgue integration. The closest non-HOL-Light formalization of a Stokes-type theorem is Abdulaziz and Paulson’s Isabelle/HOL formalization of Green’s theorem on 2-dimensional cells [14], which is a 2D specialization of Stokes; we extend that line of work to arbitrary dimension and to true differential-form pullback under smooth singular parametrizations. We are not aware of a Coq, Mizar, Metamath, or HOL4 formalization of Stokes’ theorem for singular cubes or smooth manifolds with boundary.

1.2.0.4 Paper organization.

2 presents the main singular Stokes theorem first for motivation; it depends on the box infrastructure of §§3–5, which is developed subsequently. §§6–10 give specializations and extensions. §§11–13 discuss architecture, insights, and limitations.

2 Smooth Singular Cubical Stokes↩︎

The main result of this paper is Stokes’ theorem for smooth singular cubes—a generalization of the box Stokes theorem that allows the integrand to come from a globally smooth map \(\sigma:\mathbb{R}^{n+1}\to\mathbb{R}^m\), with the integral still taken over the parameter cube \([0,1]^{n+1}\) (the box case is recovered as \(\sigma=\mathrm{id}\) on \(\mathbb{R}^{n+1}\)). No image-domain theory is formalized.

2.1 Smooth Singular Cubes↩︎

In Lean 4:⁴

structure SmoothSingularCube (n m : Nat) where
  toFun : (Fin n -> Real) -> (Fin m -> Real)
  smooth : ContDiff Real Top toFun

def faceInclusion (i : Fin (n + 1)) (eps : Real) (t : Fin n -> Real) :
    Fin (n + 1) -> Real := ...

def singularFace (sigma : SmoothSingularCube (n + 1) m)
    (i : Fin (n + 1)) (eps : Real) : SmoothSingularCube n m where
  toFun := sigma.toFun comp faceInclusion i eps
  smooth := sigma.smooth.comp (faceInclusion_contDiff i eps)

2.2 True Pullback via Fréchet Derivative↩︎

The central construction of the singular cube formalization is the use of the true differential-form pullback, defined via the Fréchet derivative. We write \(d\) for the domain dimension. In the Stokes application, \(d = n{+}1\) and \(k = n\), but the pullback definition is general:

In Lean 4, this is expressed via ContinuousAlternatingMap.compContinuousLinearMap:⁵

def pullbackForm (sigma : SmoothSingularCube d m)
    (omega : (Fin m -> Real) ->
         (Fin m -> Real) [Alt^Fin k]->L[Real] Real) :
    (Fin d -> Real) -> (Fin d -> Real) [Alt^Fin k]->L[Real] Real :=
  fun x => (omega (sigma.toFun x)).compContinuousLinearMap
              (fderiv Real sigma.toFun x)

This is genuinely the differential-geometric pullback: it applies the form \(\omega\) at the image point \(\sigma(x)\) to vectors pushed forward by the derivative \(D\sigma(x)\). This contrasts with the “coefficient precomposition” \((A \cdot \omega)_i(x) := \omega_i(Ax)\) used in the box infrastructure, which does not mix coefficients or involve determinants.

def integrateForm (sigma : SmoothSingularCube d m)
    (omega : (Fin m -> Real) ->
         (Fin m -> Real) [Alt^Fin d]->L[Real] Real) : Real :=
  integral (x in Icc (fun _ => 0) (fun _ => 1))
    (pullbackForm sigma omega x) (fun j => Pi.single j 1)

2.3 Proof Strategy↩︎

The proof of singular Stokes proceeds in three steps:

2.3.0.1 Step 1: Naturality of pullback.

The key identity is commutativity of pullback with the exterior derivative: \[\mathrm{d}(\sigma^*\omega) = \sigma^*(\mathrm{d}\omega)\] In Lean 4, this follows directly from mathlib4’s extDeriv_pullback:

theorem pullback_extDeriv (sigma : SmoothSingularCube (n + 1) m)
    (omega : ...) (h_omega : ContDiff Real Top omega)
    (x : Fin (n + 1) -> Real) :
    extDeriv (pullbackForm sigma omega) x =
    (extDeriv omega (sigma.toFun x)).compContinuousLinearMap
      (fderiv Real sigma.toFun x)

2.3.0.2 Step 2: Apply box Stokes to \(\sigma^*\omega\).

Since \(\sigma^*\omega\) is a smooth differential form on \(\mathbb{R}^{n+1}\), the existing box Stokes theorem (stokes_extDeriv, 4) applies on \([0,1]^{n+1}\): \[\int_{[0,1]^{n+1}} \mathrm{d}(\sigma^*\omega) \;=\; \int_{\partial[0,1]^{n+1}} \sigma^*\omega\] (in Lean: boxIntegral (extDerivCoord ...) = bdryIntegral ...). Smoothness of the coordinate coefficients of \(\sigma^*\omega\) is proved via toCoordNForm_pullback_isSmooth, which derives it from the global \(C^\infty\) hypotheses on \(\sigma\) and \(\omega\) using the chain rule for ContDiff.

2.3.0.3 Step 3: Face matching.

The face matching identity connects the box boundary integral of \(\sigma^*\omega\) to the face integrals of the singular cube. The core lemma is:

The proof uses the chain rule: \(D(\sigma \circ \iota_{i,\varepsilon})(x) = D\sigma(\iota_{i,\varepsilon}(x)) \circ D\iota_{i,\varepsilon}(x)\), together with the derivative identity \(D\iota_{i,\varepsilon}(x) \cdot e_j = e_{\mathrm{succAbove}(i,j)}\) (proved as fderiv_faceInclusion_single). The alternating map’s multilinearity then transforms the \(n\) basis vectors \(e_{\mathrm{succAbove}(i,0)}, \ldots, e_{\mathrm{succAbove}(i,n{-}1)}\) applied inside \(\sigma^*\omega\) into \(e_0, \ldots, e_{n-1}\) applied inside \((\sigma \circ \iota_{i,\varepsilon})^*\omega\).

2.4 The Main Theorem↩︎

The Lean statement:

theorem singularStokes (sigma : SmoothSingularCube (n + 1) m)
    (omega : (Fin m -> Real) ->
         (Fin m -> Real) [Alt^Fin n]->L[Real] Real)
    (h_omega : ContDiff Real Top omega) :
    integrateForm sigma (fun y => extDeriv omega y) =
    sum i : Fin (n + 1),
      (-1 : Real) ^ (i : Nat) *
      (integrateForm (singularFace sigma i 1) omega -
       integrateForm (singularFace sigma i 0) omega)

2.4.0.1 The theorem applies non-trivially to non-axis-aligned parametrizations.

The theorem holds for any globally smooth \(\sigma\), not only for box-aligned parametrizations. As an informal illustration (this specific computation is not formalized; it serves as a paper-only sanity check), take the polar parametrization of an annulus, \[\sigma : \mathbb{R}^2 \to \mathbb{R}^2,\qquad \sigma(r,\theta) = \bigl((1+r)\cos(2\pi\theta),\; (1+r)\sin(2\pi\theta)\bigr),\] together with the 1-form \(\omega = \tfrac{1}{2}(x\,\mathrm{d}y - y\,\mathrm{d}x)\) on \(\mathbb{R}^2\) (so \(\mathrm{d}\omega = \mathrm{d}x\wedge\mathrm{d}y\)). Because \(\sigma\) is real-analytic on all of \(\mathbb{R}^2\), the global \(C^\infty\) hypothesis of 4 is satisfied. The theorem then equates the parameter-cube integral \(\int_{[0,1]^2}\sigma^*(\mathrm{d}\omega)\) with the alternating sum of pullback integrals over the four edges of the unit square: by direct computation, the parameter-cube integrand reduces to the Jacobian \(\det D\sigma(r,\theta) = 2\pi(1+r)\), consistent with the classical Jacobian formula for area. Concretely, \(\int_0^1\!\int_0^1 2\pi(1+r)\,dr\,d\theta = 3\pi\), and the alternating face-integral sum yields the same value (the two \(\theta{=}0\) and \(\theta{=}1\) edge integrals cancel by periodicity)—providing a numerical sanity check of the theorem. The development includes LeanStokes/CubeStokes/Demo.lean, which exercises box Stokes (the specialization of 4 to \(\sigma = \mathrm{id}\)) in 4D, 5D, and 10D; the full singular theorem with non-trivial \(\sigma\) is exercised at the type-checking level via the singularStokes declaration.

2.5 Chain-Level Extension↩︎

Stokes extends by \(\mathbb{Z}\)-linearity to formal chains of singular cubes:

Chain integration satisfies additivity (integrateChain_add) and scalar compatibility (integrateChain_smul):

\[\int_{c_1 + c_2} \omega = \int_{c_1}\omega + \int_{c_2}\omega \qquad\text{and}\qquad \int_{k \cdot c}\omega = k \cdot \int_c \omega\] where \(k \in \mathbb{Z}\) acts via the canonical embedding \(\mathbb{Z}\hookrightarrow \mathbb{R}\).

3 Box Stokes: Mathematical Framework↩︎

The singular Stokes theorem reduces to the box Stokes theorem, which we now describe. This section presents the coordinate-level infrastructure that serves as the foundation for the entire development.

3.1 Coordinate \(n\)-Forms on \(\mathbb{R}^{n+1}\)↩︎

An \(n\)-form on \(\mathbb{R}^{n+1}\) can be written in coordinates as: \[\omega = \sum_{i=0}^{n} \omega_i(x)\, \mathrm{d}x_0 \wedge \cdots \wedge \widehat{\mathrm{d}x_i} \wedge \cdots \wedge \mathrm{d}x_n\] where \(\widehat{\mathrm{d}x_i}\) denotes omission. We represent this as a family of coefficient functions:

In Lean 4:

def CoordNForm (n : Nat) := Fin (n + 1)  ->  (Fin (n + 1)  ->  Real)  ->  Real

3.2 Exterior Derivative↩︎

The exterior derivative of \(\omega\) is the \((n{+}1)\)-form (i.e., a top form on \(\mathbb{R}^{n+1}\)): \[\mathrm{d}\omega = \left(\sum_{i=0}^{n} (-1)^i \frac{\partial\omega_i}{\partial x_i}\right) \mathrm{d}x_0 \wedge \cdots \wedge \mathrm{d}x_n\]

The key insight for our proof is the signed coefficient construction:

The sign arises because \(\mathrm{d}(\omega_i\,\mathrm{d}x_0\wedge\cdots \wedge\widehat{\mathrm{d}x_i}\wedge\cdots\wedge\mathrm{d}x_n)\) requires \(i\) adjacent transpositions to place \(\mathrm{d}x_i\) in position \(i\), yielding the factor \((-1)^i\). With this convention, the exterior derivative coefficient becomes the divergence of the vector field \((f_0, \ldots, f_n)\): \[\mathrm{d}\omega = \left(\sum_{i=0}^{n} \frac{\partial f_i}{\partial x_i}\right) \mathrm{d}x_0 \wedge \cdots \wedge \mathrm{d}x_n\]

This is precisely what mathlib4’s divergence theorem computes.

3.3 Boundary Integral↩︎

For a box \([a, b] = \prod_{i=0}^{n} [a_i, b_i] \subset \mathbb{R}^{n+1}\), the oriented boundary integral of \(\omega\) is: \[\int_{\partial[a, b]} \omega = \sum_{i=0}^{n} \left( \int_{\text{face}_i} f_i(b_i, \hat{x}_i)\, \mathrm{d}\hat{x}_i - \int_{\text{face}_i} f_i(a_i, \hat{x}_i)\, \mathrm{d}\hat{x}_i \right)\] where \(\text{face}_i = \prod_{j \neq i} [a_j, b_j]\) is the \(n\)-dimensional face box, \(\hat{x}_i = (x_0, \ldots, x_{i-1}, x_{i+1}, \ldots, x_n)\) denotes all coordinates except \(i\), and \(f_i(c, \hat{x}_i)\) denotes inserting \(c\) at position \(i\).

This exactly matches the right-hand side of mathlib4’s divergence theorem.

4 Box Stokes: Main Theorem↩︎

The Lean statement:

theorem stokes_on_box (a b : Fin (n + 1)  ->  Real) (hle : a  <=  b)
    (omega : CoordNForm n)
    (s : Set (Fin (n + 1)  ->  Real)) (hs : s.Countable)
    (hc : forall  i, ContinuousOn (signedCoeff omega i) (Icc a b))
    (hd : forall  x  in  (pi univ fun i => Ioo (a i) (b i)) \;s,
      forall  i, HasFDerivAt (signedCoeff omega i)
        ((-1 : Real) ^ (i : Nat)  smul  fderiv Real (omega i) x) x)
    (hi : IntegrableOn (fun x => Finset.sum i : Fin (n + 1),
      ((-1 : Real) ^ (i : Nat)  smul  fderiv Real (omega i) x) (Pi.single i 1))
      (Icc a b)) :
    boxIntegral (extDerivCoord omega) a b = bdryIntegral omega a b

  unfold boxIntegral bdryIntegral extDerivCoord
  exact integral_divergence_of_hasFDerivAt_off_countable'
    a b hle (signedCoeff omega)
    (fun i x => (-1 : Real) ^ (i : Nat)  smul  fderiv Real (omega i) x)
    s hs hc hd hi

theorem stokes_smooth (a b : Fin (n + 1)  ->  Real) (hle : a  <=  b)
    (omega : CoordNForm n) (homega : IsSmooth omega) :
    boxIntegral (extDerivCoord omega) a b = bdryIntegral omega a b

5 Bridge: From mathlib4 Exterior Derivative to Box Stokes↩︎

The bridge theorem validates our coordinate formula against mathlib’s independently-defined abstract exterior derivative. It proves that evaluating mathlib4’s extDeriv—defined via Fréchet derivatives of alternating maps—on standard basis vectors recovers our coordinate extDerivCoord, confirming that the sign convention is mathematically correct. This does not establish a full theory of form integration or pullbacks, but it provides the independent consistency guarantee a referee would expect.

The proof uses extDeriv_apply_vectorField_of_pairwise_commute with constant vector fields \(V_j(x) = e_j\), which have zero Lie bracket. This mathlib4 lemma expresses \((\mathrm{d}\omega)(V_0, \ldots, V_n)\) as an alternating sum of directional derivatives \(V_j[\omega(V_0, \ldots, \widehat{V_j}, \ldots, V_n)]\); the Lie bracket terms vanish because the \(V_j\) are constant:

theorem extDeriv_topCoeff_eq_extDerivCoord
    (omega : (Fin (n + 1)  ->  Real)  -> 
         (Fin (n + 1)  ->  Real) [Alt^Fin n] -> L[Real] Real)
    (x : Fin (n + 1)  ->  Real)
    (homega : DifferentiableAt Real omega x) :
    extDeriv omega x (fun j => Pi.single j 1)
      = extDerivCoord (toCoordNForm omega) x

theorem stokes_extDeriv_smooth
    (omega : (Fin (n + 1)  ->  Real)  -> 
         (Fin (n + 1)  ->  Real) [Alt^Fin n] -> L[Real] Real)
    (a b : Fin (n + 1)  ->  Real) (hle : a  <=  b)
    (homega : ContDiff Real Top omega) :
    integral (x in Icc a b) (extDeriv omega x (fun j => Pi.single j 1))
      = bdryIntegral (toCoordNForm omega) a b

6 Dimensional Specializations↩︎

Each result below is a box/interval specialization of stokes_smooth (a direct dimensional instantiation, not an independent derivation):

6.1 1D Agreement Check↩︎

A natural concern with the coordinate approach is whether the Stokes theorem produces correct integral values. We validate this for the 1D case (\(n{=}0\), the FTC) by computing via two independent paths and showing they agree:

1. Path 1 (Stokes): stokes_smooth \(\to\) ftc_stokes \(\to\) \(f(b) - f(a)\)

2. Path 2 (interval integral):
   intervalIntegral.integral_eq_sub_of_hasDerivAt \(\to\) ftc_intervalIntegral \(\to\) \(f(b) - f(a)\)

The agreement theorem (ftc_paths_agree) shows both paths produce the same result. The Stokes path uses set integrals over \(\mathrm{Fin}\,1 \to \mathbb{R}\) of \(\mathrm{fderiv}\), while the interval-integral path uses mathlib’s direct FTC (intervalIntegral.integral_eq_sub_of_hasDerivAt). Their agreement provides a sanity check that our box-integral machinery computes standard calculus integrals correctly in the \(n{=}0\) case, though both paths ultimately rely on mathlib’s analysis library (the divergence theorem for path 1, direct FTC for path 2). The validation is therefore a consistency check of our definitions and sign conventions against mathlib’s independent FTC path, not a check of mathlib’s analysis foundations themselves.

7 Formal Sums and Linear Extension↩︎

We define formal \(\mathbb{Z}\)-linear combinations of boxes and extend Stokes by linearity:

Integration extends linearly to chains:

def integrateExterior (c : CubicalChain n) (omega : CoordNForm n) : Real :=
  c.sum fun B k => (k : Real) * boxIntegral (extDerivCoord omega) B.lo B.hi

Additivity properties (integrateExterior_add, integrateBdry_add) are proved via Finsupp.sum_add_index'.

7.1 Two-Box Additivity and Shared-Face Cancellation↩︎

A natural question is whether the Stokes identity is compatible with decomposing a box into two adjacent sub-boxes. The subdivision module shows that for any two boxes (forming a 2-element chain), the Stokes identity holds for the combined chain:

This is proved as a direct consequence of the single-box Stokes theorem (by linarith). The chain-level version (stokes_two_boxes) follows from stokes_chain.

We additionally formalize the key shared-face cancellation:

7.2 Paired Codimension-2 Face Cancellation↩︎

The fundamental property of the boundary operator in a chain complex is \(\partial^2 = 0\): applying the boundary twice gives zero. We prove the sign-arithmetic core of this identity: for each codimension-2 face in the double boundary, the two paths that reach it produce opposite signed contributions. This is the essential algebraic content of \(\partial^2 = 0\), though we do not define \(\partial\) as a chain-group homomorphism (our undecorated box type does not distinguish upper/lower faces as separate chain elements).

8 Algebraic Properties↩︎

The exterior derivative extDerivCoord is a linear operator:

Combined with Stokes, these give:

theorem stokes_smooth_add (a b) (hle : a <= b) (omega eta) (ho he) :
    boxIntegral (extDerivCoord (CoordNForm.add omega eta)) a b =
    bdryIntegral (CoordNForm.add omega eta) a b

9 Coefficient Precomposition by Linear Maps↩︎

For coordinate forms on boxes, we additionally provide precomposition of coefficients by continuous linear maps and prove functoriality. We emphasize that this is coefficient-wise precomposition \((A \cdot \omega)_i(x) := \omega_i(Ax)\), which is not the true exterior-algebraic pullback used in 2: the true pullback acts via the full Fréchet derivative and mixes coefficients, while coefficient precomposition merely pre-composes each coefficient function individually.

The development includes the expected lemmas: smoothness preservation under continuous linear \(A\) (pullback_smooth, proved via ContDiff.comp); contravariant functoriality \((A \cdot (B \cdot \omega)) = (B \circ A) \cdot \omega\) (pullback_comp); identity \(\mathrm{id}\cdot\omega = \omega\) (pullback_id); linearity in \(\omega\) (pullback_add, pullback_smul); and a Stokes specialization for precomposed forms (stokes_pullback), which follows immediately from stokes_smooth applied to \(A\cdot\omega\). We do not claim that this operation commutes with the exterior derivative in general; it satisfies Stokes only because Stokes holds for every smooth coordinate form, regardless of its origin.

10 The \(d^2{=}0\) Identity from mathlib4↩︎

A fundamental property of the exterior derivative is nilpotency: \(d(d\omega) = 0\). We derive this at the coordinate level through our bridge to mathlib4:

10.1 Boundary Operator: Face-of-Face Identities↩︎

We formalize the sign-arithmetic and geometric core underlying \(\partial^2 = 0\) at the box level. For a box \(B \subset \mathbb{R}^{n+3}\), the double boundary \(\partial^2 B\) consists of codimension-2 faces, each appearing via two paths:

• Path 1: face \(j\) of (face \(i\) of \(B\))

• Path 2: face \((\mathrm{predAbove}\;j\;i)\) of (face \((\mathrm{succAbove}\;i\;j)\) of \(B\))

Together these establish the face-of-face composition identity and sign-arithmetic core of \(\partial^2 = 0\): each codimension-2 face appears with opposite signs in the double boundary. However, this is not a full \(\partial^2 = 0\) at the chain level, since we do not define \(\partial\) as a chain-group homomorphism (our undecorated box type does not distinguish upper/lower faces as separate chain elements).

10.2 Chain-Level \(\partial^2 = 0\) for Singular Cubes↩︎

In the smooth singular cube module, we do prove the full chain complex identity \(\partial^2 = 0\) for singular chains (cf. the textbook treatment in [16]). Here the boundary operator \(\partial\) is a genuine \(\mathbb{Z}\)-linear map \(\partial : C_{n+1}(\mathbb{R}^m) \to C_n(\mathbb{R}^m)\) between singular chain groups.

10.2.0.1 Proof strategy.

The proof uses a sign-reversing fixed-point-free involution on the index set \(\mathrm{Fin}(n{+}2) \times \mathrm{Fin}(n{+}1)\) of the double sum, combined with Finset.sum_ninvolution from mathlib4.

The involution maps: \[g(i, j) = \begin{cases} (j{+}1,\; i) & \text{if } i \leq j \\ (j,\; i{-}1) & \text{if } i > j \end{cases}\]

For each pair \((i,j)\) with \(i \leq j\), the cancellation argument has two components:

1. Same cube: The face-of-face identity (singularFace_comp) shows that \(\mathrm{face}_j(\delta, \mathrm{face}_i(\varepsilon, \sigma)) = \mathrm{face}_i(\varepsilon, \mathrm{face}_{j+1}(\delta, \sigma))\), so paired terms produce the same singular cube.

2. Opposite sign: The coefficients \((-1)^i(-1)^j\) and \((-1)^{j+1}(-1)^i\) satisfy \((-1)^{i+j} + (-1)^{i+j+1} = 0\).

After applying the face-of-face identity, the proof uses ext\(\tau\); simp [Finsupp.single_apply]; split_ifs <;> ring to close all 256 goals of the split case analysis automatically (goal count observed with Lean 4.29.1; may vary across versions).

This establishes that \((\{C_n(\mathbb{R}^m)\}, \partial)\) forms a genuine chain complex. Combined with stokes_chain, this yields the identity one would use to define integration as a cochain map from the de Rham complex to singular cubical cochains; however, we do not formally package these complexes or prove the commuting-square diagram as a Lean structure.

11 Architecture and Infrastructure↩︎

11.1 Module Structure↩︎

The formalization consists of 44 Lean 4 source files in the LeanStokes/ directory totaling 4028 source lines, plus a root import file LeanStokes.lean. Selected modules and their roles:

All modules are sorry-free.

11.2 Design Decisions↩︎

11.2.0.1 Dimension indexing.

We use Fin (n + 1) for the ambient dimension, avoiding the subtraction issue where (d - 1) + 1 \(\neq\) d in natural number arithmetic.

11.2.0.2 Signed coefficients.

The key insight enabling the 3-line proof is defining \(f_i(x) = (-1)^i \omega_i(x)\), so that:

• \(\mathrm{div}(f) = \sum_i \partial f_i / \partial x_i\), which equals the single coefficient of the top-form \(\mathrm{d}\omega\)

• The divergence theorem’s boundary terms match our boundary integral

11.2.0.3 Separation of concerns.

The general theorem (stokes_on_box) takes explicit hypotheses about continuity, differentiability, and integrability. The smooth version (stokes_smooth) derives these automatically from ContDiff Real Top.

11.3 Axiom Audit↩︎

Every key theorem was verified via \#print axioms (79 declarations checked, covering all main results and their transitive dependencies). All produce the same axiom set:

• propext (propositional extensionality)

• Classical.choice (classical logic)

• Quot.sound (quotient soundness)

These are the standard axioms of Lean 4’s foundation, present in all nontrivial mathlib4 proofs. No sorry or additional axioms are used.

12 Formalization Insights and Challenges↩︎

This section describes what the formalization process revealed about the mathematics of Stokes’ theorem and cubical chains. We present both “what was proved” and “what was learned,” following established practice in formalization papers [11], [12].

12.1 The Bridge Pattern: Connecting Concrete and Abstract↩︎

The most reusable methodological contribution of this work is the bridge theorem pattern. mathlib4’s extDeriv operates on ContinuousAlternatingMap-valued functions in full generality, while our box-level infrastructure uses coordinate-indexed functions \(\omega_i : \mathbb{R}^{n+1} \to \mathbb{R}\). The bridge theorem (stokes_extDeriv_smooth, 5) proves that evaluating the abstract extDeriv on standard basis vectors recovers our coordinate formula.

This pattern—where a concrete computational representation is validated against an abstract library definition—may be reusable wherever formalizers face the choice between “build from scratch in a concrete representation” and “use the library’s abstract API directly” [17]. The bridge makes both approaches compatible.

12.2 Pitfall: Nat Subtraction in Sign Exponents↩︎

A recurring obstacle in the chain-level \(\partial^2 = 0\) proof was Lean 4’s treatment of natural-number subtraction in exponents. The ring tactic cannot simplify \((-1)^{n-1}\) when \(n\) is a natural-number variable, because \(n - 1\) is not a polynomial operation (it truncates to 0 when \(n = 0\)).

Our solution was the helper lemma neg_one_pow_pred: for \(n > 0\), \((-1 : \mathbb{Z})^{n-1} = -(-1)^n\). This allows simp only [neg_one_pow_pred ...] to preprocess sign expressions before ring closes the goal. This illustrates a general principle: ring-normalizable expressions must avoid Nat subtraction, and dedicated lemmas are needed to bridge the gap.

12.3 Pitfall: Fin Projection Opacity↩︎

Lean 4’s kernel does not always reduce \((\langle e, h\rangle : \mathrm{Fin}\;n).val\) to \(e\) during unification. This caused repeated failures when proving equalities involving composed face maps (e.g., \(\mathrm{faceInclusion}\;i\;\varepsilon \circ \mathrm{faceInclusion}\;j\;\delta\)). The solution is explicit use of Fin.val_mk or dsimp to force projection reduction before omega can close the arithmetic goal.

12.4 Insight: Why Global Smoothness Simplifies Everything↩︎

We require singular cubes to be globally \(C^\infty\) (not just smooth on \([0,1]^{n+1}\)). This is mathematically stronger than necessary but has a cascade of simplification effects:

1. ContDiff composes freely: \(\sigma \circ \iota_{i,\varepsilon}\) is automatically \(C^\infty\) without boundary regularity arguments.

2. fderiv is well-defined everywhere, avoiding the need for HasFDerivAt hypotheses localized to the cube interior.

3. The pullback \(\sigma^*\omega\) is smooth on all of \(\mathbb{R}^{n+1}\), so box Stokes applies directly without restriction arguments.

A formalization that required smoothness only on the cube would need ContDiffOn (which composes less freely) and careful bookkeeping of open neighborhoods—substantial additional infrastructure with no mathematical payoff for the theorem statement.

12.5 Insight: extDeriv_pullback as the Key Enabler↩︎

Without mathlib4’s extDeriv_pullback, the singular Stokes theorem would have been substantially harder. That single theorem provides \(d(\sigma^*\omega) = \sigma^*(d\omega)\) pointwise and reduces singular Stokes to box Stokes in three steps: (1) apply naturality, (2) apply box Stokes to the pullback, (3) match faces. Without it we would have had to reprove naturality of the exterior derivative under pullback—a substantial undertaking involving the Leibniz rule for wedge products and the composition of multilinear maps.

12.6 The Involution Method for \(\partial^2 = 0\)↩︎

The chain-level \(\partial^2 = 0\) proof uses Finset.sum_ninvolution: to show \(\sum_{p \in S} f(p) = 0\), it suffices to find a fixed-point-free involution \(g : S \to S\) such that \(f(p) + f(g(p)) = 0\) for all \(p\). This is a standard combinatorial technique, but its application to cubical boundary algebra required careful construction: the involution \(g(i,j) = (j{+}1, i)\) when \(i \leq j\) and \((j, i{-}1)\) otherwise produces 256 case-split goals in the cancellation proof, all of which close with ring after sign preprocessing.

The mathematical lesson is that \(\partial^2 = 0\) for cubical chains is fundamentally a combinatorial identity (sign-reversing involution on index pairs) rather than an algebraic identity (in the sense of ring operations). The formal proof makes this distinction precise in a way informal proofs typically obscure.

13 Discussion↩︎

13.1 Scope and Limitations↩︎

Our formalization proves Stokes’ theorem at two levels: (1) for smooth singular cubes—globally \(C^\infty\) maps \(\sigma : \mathbb{R}^{n+1} \to \mathbb{R}^m\) integrated over \([0,1]^{n+1}\) with true pullback via fderiv—and (2) for axis-aligned boxes and their formal \(\mathbb{Z}\)-linear combinations. We state the concrete limitations explicitly:

• No manifolds or partitions of unity: The integration domain is always \([0,1]^{n+1}\) (or \([a, b]\) for boxes). No charts, atlases, smooth structures, or partition-of-unity arguments are used. Singular cubes must be single smooth parametrizations.

• Global smoothness: Singular cubes are required to be \(C^\infty\) on all of \(\mathbb{R}^{n+1}\), not just on \([0,1]^{n+1}\). This is stronger than necessary mathematically, but simplifies the formalization.

• Box-level form degree: The box-level infrastructure handles only coordinate \(n\)-forms on \(\mathbb{R}^{n+1}\) (one degree below top). The pullback construction is defined for arbitrary form degree \(k\); the singular Stokes theorem applies to \(n\)-forms integrated over smooth singular \((n{+}1)\)-cubes.

• Box Stokes reduces to divergence theorem: The core box theorem reduces to mathlib4’s divergence theorem. The mathematical content is in the sign-convention construction, the bridge to extDeriv, and the singular-cube extension via extDeriv_pullback.

• No image-domain semantics: \(\int_\sigma \omega\) is defined as an integral over \([0,1]^d\) of the pullback. We do not prove that \(\sigma([0,1]^d)\) is a submanifold or oriented geometric chain. The singular-cube module does achieve a genuine chain-complex structure: \(\partial^2 = 0\) is proved as a Finsupp identity (bdry_bdry_chain_zero).

Despite these limitations, the formalization provides:

1. True pullback of differential forms via the Fréchet derivative—the standard differential-geometric operation.

2. Smooth singular parametrizations: Singular cubes provide smooth parametrizations of curves, surfaces, and higher-dimensional objects in \(\mathbb{R}^m\), not just axis-aligned boxes. We do not prove image-domain theory (e.g., that the image is a submanifold).

3. Genuinely \(n\)-dimensional results for arbitrary \(n\) (instantiated in demos up to \(n{=}9\), i.e., 10D).

4. A bridge theorem validated against mathlib4’s abstract extDeriv.

5. Two-box additivity with shared-face cancellation showing composability.

6. 1D agreement check confirming correct integral values for the FTC case.

7. Reusable infrastructure: the singular-cube framework, face matching, coordinate forms, and the bridge pattern may serve as building blocks for further development.

13.2 What Remains for Full Manifold Stokes↩︎

A formalization of Stokes on smooth manifolds with boundary [3] would additionally require:

1. Integration of forms on manifolds: defining \(\int_M \omega\) via partition of unity and chart pullbacks.

2. Boundary orientation: the induced orientation on \(\partial M\) from the outward normal.

3. Change of variables for forms: proving that the integral is chart-independent.

4. Stokes on half-spaces: the local compactly-supported version.

5. Singular chains on manifolds: extending our singular cube infrastructure to manifold-valued maps.

Each of these is a substantial formalization project in its own right. Our singular cube framework provides a natural starting point: once manifold charts and partition of unity are available, singular cubes may serve as the local parametrizations over which Stokes is applied.

13.3 Comparison with HOL Light↩︎

Harrison’s HOL Light formalization [1] is the closest prior work. A key finding of our investigation is that Harrison’s development proves Stokes for convex and polyhedral domains extended to polyhedral chains—not for arbitrary smooth manifolds with boundary, as some secondary sources suggest.

With the addition of singular cubes, the mathematical scope of our development is complementary to Harrison’s: Harrison’s singular simplices/polytopes are parametrized by smooth maps from convex domains; our singular cubes are parametrized by smooth maps from the unit cube. Harrison has strictly broader geometric domain coverage (convex polytopes with simplicial decomposition); our contribution is a Lean 4/mathlib4 formalization with direct bridge to extDeriv and reuse of extDeriv_pullback. Both use the true differential-form pullback.

The distinguishing feature of our approach is the bridge to mathlib4’s abstract exterior algebra and the use of extDeriv_pullback for the singular theorem. We are not aware of a directly comparable bridge to an independently developed abstract exterior-derivative API in HOL Light, since HOL Light does not maintain an independent abstract exterior algebra alongside its integration theory. This means our infrastructure is directly connected to the abstract theory and may benefit from future growth in mathlib4’s manifold integration API.

Harrison’s advantage is strictly broader domain generality: convex polytopes include simplices and other non-cubical shapes. Our singular cubes always have the unit cube as the parameter domain; the smooth map \(\sigma\) can produce many parametrized images (possibly degenerate or self-overlapping), but the theorem remains a statement about integration over the parameter cube, not over the image as a domain.

13.4 Reproducibility↩︎

The complete formalization is available at:

A Software Heritage archive (SWHID) will be deposited prior to publication. It builds with Lean 4.29.1 and mathlib4 (pinned to rev = "v4.29.1" in lakefile.toml; both version pins are in the repository). To verify:

  lake exe cache get && lake build

Representative \#print axioms output (all checked theorems produce the same three axioms):

'SingularCubeStokes.singularStokes' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'CubeStokes.stokes_on_box' depends on axioms:
  [propext, Classical.choice, Quot.sound]
'SingularCubeStokes.stokes_singular_boundary' depends on axioms:
  [propext, Classical.choice, Quot.sound]

14 Conclusion↩︎

We have presented a sorry-free Lean 4 formalization of Stokes’ theorem for smooth singular cubes and axis-aligned boxes in arbitrary dimension, comprising 44 modules with 205 named declarations across approximately 4000 source lines. All results depend only on the standard axioms (propext, Classical.choice, Quot.sound), confirmed by 79 \#print axioms checks covering both the box and singular cubical layers.

The headline theorem—Stokes for smooth singular cubes with true differential-form pullback—reduces to the box theorem in three steps: naturality of the pullback under the exterior derivative (\(\mathrm{d}(\sigma^*\omega) = \sigma^*(\mathrm{d}\omega)\), from mathlib4’s extDeriv_pullback), box Stokes applied to \(\sigma^*\omega\), and a chain-rule face-matching identity. The same machinery extends by \(\mathbb{Z}\)-linearity to singular chains, on which we prove \(\partial(\partial\sigma)=0\) via a sign-reversing involution on the double-boundary index set.

14.0.0.1 What we hope is reusable.

Three ingredients seem most likely to be useful for downstream formalizations: (i) the bridge theorem pattern, which validates a concrete coordinate formula against an abstract library definition; (ii) the face matching identity relating box-boundary integrals of pullback forms to face integrals of singular cubes; and (iii) the involution-based proof of \(\partial^2 = 0\) on singular cubical chains.

14.0.0.2 What remains.

A full Lean 4 formalization of Stokes for smooth manifolds with boundary still requires integration of forms via partition of unity and chart pullbacks, boundary orientation, and image-domain singular chains. Our singular-cube framework provides a natural local building block for such an effort once mathlib4’s manifold integration API matures.

The artifact is reproducible via lake exe cache get && lake build and is available at https://github.com/d0d1/lean-stokes-theorem under GPL-3.0-only, with versions pinned via lean-toolchain and lakefile.toml.

14.0.0.3 Acknowledgments.

We thank the mathlib4 community for maintaining the mathematical library on which this work depends, and the Lean 4 developers for the proof assistant infrastructure.

References↩︎