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

技術的サマリー：Lean 4 における滑らかな特異立方体に対するストークスの定理

問題提起
2026 年 4 月現在、Lean 4 のエコシステム（特に mathlib4）には、境界付き滑らかな多様体上の微分形式、あるいは特異鎖に対するストークスの定理の完全な形式化が存在しなかった。mathlib4 は軸に平行な箱に対する発散定理と抽象的な外微分（extDeriv）を有していたが、単位立方体から任意のユークリッド空間への滑らかな写像（滑らかな特異立方体）による微分形式の引き戻しを積分し、それを境界面での積分の交互和と等置する定理は未だ提供されていなかった。ハリソンによる HOL Light における既存の形式化は、凸多面体領域を扱っていたが、滑らかな特異パラメータ化や mathlib4 の抽象的外代数の特定の基盤には対応していなかった。

手法
著者らは、座標に基づく積分と抽象的な微分幾何学の間のギャップを埋める「sorry-free」（証明されていない仮定がゼロ）な形式化を提示する。この開発は、以下の 3 つの主要な方法論的柱に依存している：

1. フレシェ微分による真の引き戻し：核心的な構成は、全体的に $C^\infty$ である写像 $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ のフレシェ微分（fderiv）を用いて、微分形式 $\sigma^*\omega$ の引き戻しを定義するものである。単なる係数の事前合成とは異なり、この定義は像点 $\sigma(x)$ における形式を、$D\sigma(x)$ によって押し出されたベクトルに適用するものであり、標準的な微分幾何学的定義に準拠している。
2. 箱型ストークスへの還元：証明戦略は、特異な場合を軸に平行な箱の場合に還元する。mathlib4 の extDeriv_pullback 定理を活用することで、著者らは自然性恒等式 $d(\sigma^*\omega) = \sigma^*(d\omega)$ を確立する。これにより、既存の箱型ストークスの定理（mathlib4 の発散定理から導出されたもの）を、パラメータ領域 $[0,1]^{n+1}$ 上の引き戻された形式 $\sigma^*\omega$ に適用することが可能になる。
3. 面の整合性と鎖レベルの代数：重要な技術的要素は「面整合恒等式」であり、これは箱の境界面における引き戻された形式の積分が、対応する特異面における形式の積分と完全に一致することを証明するものである。さらに、著者らは特異鎖に対する鎖複体恒等式 $\partial(\partial\sigma) = 0$ を形式化する。これは装飾されていない箱上の境界準同型を定義するのではなく、二重境界のインデックス集合上の符号反転かつ固定点を持たない対合を構成し、対になった項が代数的に相殺されることを証明することで達成される。

主要な貢献
本論文は、44 の Lean モジュール（約 4,000 行）と 205 の命名された宣言からなる包括的な形式化を提供する。具体的な貢献は以下の通りである：

• 特異ストークスの定理：任意の全体的に $C^\infty$ である写像 $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ と任意の $C^\infty$ な $n$-形式 $\omega$ に対して、単位立方体上の $\sigma^*(d\omega)$ の積分は、$2(n+1)$ 個の面における $\sigma^*\omega$ の積分の交互和に等しいとする定理。
• 橋渡し定理：著者らの座標に基づく外微分（extDerivCoord）が、標準基底ベクトル上で評価された際に mathlib4 の抽象的な extDeriv と整合的であることを検証する形式的証明。これにより、座標実装がライブラリの抽象 API に対して数学的に妥当であることが保証される。
• 鎖レベルの拡張：線形性を通じて、特異立方体の形式的な $\mathbb{Z}$-線形結合（特異鎖）へのストークスの定理の拡張。
• $\partial^2 = 0$ の証明：二重面のインデックス集合上の組み合わせ論的対合を用いた、特異鎖に対する鎖複体恒等式 $\partial(\partial\sigma) = 0$ の形式的証明。
• 次元特殊化：微積分の基本定理（FTC）、グリーン定理、発散定理、3 次元ガウスの定理、および部分積分とライプニッツ則を回復する、主要定理の直接インスタンス化。
• 公理監査：開発全体が 3 つの標準的な Lean 4 の公理（propext、Classical.choice、Quot.sound）のみに依存していることの検証。これは 79 回の体系的な #print axioms チェックによって確認された。

結果と範囲
この形式化は、以下の対象に対してストークスの定理の証明に成功している：

1. 滑らかな特異立方体：$\mathbb{R}^{n+1}$ 上で全体的に滑らかな写像 $\sigma$ を、パラメータ立方体 $[0,1]^{n+1}$ 上で積分したもの。
2. 軸に平行な箱：箱 $[a,b] \subset \mathbb{R}^{n+1}$ 上の座標 $n$-形式。

本論文は、以下の制限と範囲の境界を明示的に指摘している：

• 多様体理論の不在：積分領域は厳密にパラメータ立方体または箱である。この研究は一般的な滑らかな多様体上の積分を形式化しておらず、単位分割、座標近傍、またはアトラスも使用していない。
• 全体的な滑らかさ：特異写像は閉じた立方体上だけでなく、$\mathbb{R}^{n+1}$ 全体で $C^\infty$ であることが要求される。これは立方体上でのみ滑らかであるという条件よりも強い条件である。この選択は、境界正則性の議論を回避し、フレシェ微分が至る所で well-defined であることを保証することで、形式化を単純化するためになされた。
• 像領域の意味の不在：この定理は積分をパラメータ領域上の演算として扱う。$\sigma$ の像が目標空間における部分多様体または向き付けられた幾何学的鎖を構成することを証明するものではない。

意義と主張
著者らは、この研究が「真の」微分形式の引き戻しを伴う滑らかな特異立方体に対するストークスの定理の、最初の完全な Lean 4 形式化を提供すると主張する。その意義は以下の点にある：

1. 具体的と抽象的な橋渡し：「橋渡し定理」のパターンは、mathlib4 の抽象的な外微分に対して具体的な座標実装を検証し、将来の形式化のための再利用可能な方法論を提供する。
2. インフラの再利用：この開発は既存の mathlib4 インフラ（発散定理、extDeriv_pullback）に大きく依存しており、基礎的な解析を再考することなく、高レベルのライブラリ構成要素を組み合わせることで複雑な幾何学的定理を証明できることを示している。
3. 相補性：この研究はハリソンの HOL Light 形式化と相補的である。ハリソンはゲージ積分を用いて凸・多面体領域を扱うのに対し、この研究はボホナー積分と mathlib4 の微分幾何学 API を用いて滑らかな特異パラメータ化を扱う。
4. 基礎的準備：$\partial^2=0$ を証明し、鎖レベルのストークスの定理を確立することで、著者らは将来、mathlib4 の多様体積分と向き付け API が成熟した際に、境界付き滑らかな多様体上のストークスの定理の完全な形式化に向けた必要な局所的な構築ブロックを提供している。

本論文は、一般的な多様体上の積分の問題を解決するものではないが、真の引き戻しを伴う重要な「立方体鎖」層を確立し、将来の拡張のための検証済みの基盤として機能すると結論付けている。