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) 을 보유하고 있었지만, 매끄러운 특이 큐브 (단위 큐브에서 임의의 유클리드 공간으로의 매끄러운 사상) 에 대한 미분 형식의 당김 (pullback) 적분과 이를 경계 면에 대한 적분의 교대 합과 동일시하는 정리는 아직 제공되지 않았습니다. Harrison 의 HOL Light 에서의 작업과 같은 기존 형식화들은 볼록 및 다면체 영역을 다루었지만, 매끄러운 특이 매개화나 mathlib4 의 추상적 외대수 인프라에 대한 구체적인 내용은 다루지 않았습니다.

방법론
저자들은 좌표 기반 적분과 추상 미분 기하학 사이의 간극을 메우는 "sorry-free" (미증명 가정 0 개) 형식화를 제시합니다. 이 개발은 세 가지 주요 방법론적 기둥에 의존합니다:

1. 프레셰 미분을 통한 진정한 당김: 핵심 구성은 전역적으로 $C^\infty$ 인 사상 $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ 의 프레셰 미분 ($fderiv$) 을 사용하여 미분 형식$\sigma^*\omega$의 당김을 정의합니다. 단순한 계수 사전 합성과 달리, 이 정의는 이미지 점$\sigma(x)$에서의 형식을$D\sigma(x)$ 에 의해 밀어올려진 (pushed forward) 벡터에 적용하여 표준 미분 기하학적 정의에 부합합니다.
2. 박스 스토크스로의 축소: 증명 전략은 특이 사례를 축 정렬 박스 사례로 축소합니다. mathlib4 의 extDeriv_pullback 정리를 활용하여 저자들은 자연성 항등식 $d(\sigma^*\omega) = \sigma^*(d\omega)$ 를 확립합니다. 이를 통해 기존 박스 스토크스 정리 ( mathlib4 의 발산 정리에서 유도됨) 를 매개변수 영역 $[0,1]^{n+1}$ 위의 당겨진 형식 $\sigma^*\omega$ 에 적용할 수 있게 됩니다.
3. 면 매칭 및 사슬 수준 대수: 중요한 기술적 구성 요소는 "면 매칭 항등식"으로, 이는 박스 경계 면에 대한 당겨진 형식의 적분이 해당 특이 면에 대한 형식의 적분과 정확히 일치함을 증명합니다. 또한 저자들은 특이 사슬에 대한 사슬 복합체 항등식 $\partial(\partial\sigma) = 0$ 을 형식화합니다. 이는 장식되지 않은 박스에 대한 경계 준동형을 정의하는 것이 아니라, 이중 경계 인덱스 집합에 대한 부호 반전 고정점 없는 대합 (involution) 을 구성하여 짝지어진 항들이 대수적으로 상쇄됨을 증명함으로써 달성됩니다.

주요 기여
본 논문은 약 4,000 줄의 44 개 Lean 모듈과 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 차원 가우스 정리, 그리고 부분적분과 라이프니츠 법칙을 복원하는 주요 정리의 직접적 인스턴스화.
• 공리 감사: 전체 개발이 세 가지 표준 Lean 4 공리 (propext, Classical.choice, Quot.sound) 에만 의존함을 79 개의 체계적인 #print axioms 검사를 통해 확인.

결과 및 범위
이 형식화는 다음에 대해 스토크스 정리의 증명을 성공적으로 수행합니다:

1. 매끄러운 특이 큐브: $\mathbb{R}^{n+1}$ 에서 전역적으로 매끄러운 사상 $\sigma$ 를 매개변수 큐브 $[0,1]^{n+1}$ 위에서 적분한 경우.
2. 축 정렬 박스: $\mathbb{R}^{n+1}$ 의 박스 $[a,b]$ 위의 좌표 $n$-형식.

본 논문은 다음과 같은 한계와 범위 경계를 명시적으로 지적합니다:

• 다양체 이론 부재: 적분 영역은 엄격하게 매개변수 큐브 또는 박스입니다. 이 작업은 일반적인 매끄러운 다양체 위의 적분을 형식화하지 않으며, 단위 분할, 좌표계, 또는 아틀라스를 사용하지 않습니다.
• 전역 매끄러움: 특이 사상은 닫힌 큐브 자체뿐만 아니라 전체 $\mathbb{R}^{n+1}$ 에서 $C^\infty$ 이어야 합니다. 이는 경계 정규성 논증을 피하고 프레셰 미분이 모든 곳에서 잘 정의되도록 하여 형식화를 단순화하기 위해 선택된 조건입니다.
• 이미지-영역 의미론 부재: 이 정리는 적분을 매개변수 영역에 대한 연산으로 취급합니다. $\sigma$ 의 이미지가 타겟 공간에서 부분 다양체 또는 방향이 부여된 기하학적 사슬을 구성함을 증명하지는 않습니다.

의의 및 주장
저자들은 이 작업이 "진정한" 미분 형식 당김을 갖춘 매끄러운 특이 큐브에 대한 스토크스 정리의 첫 번째 완전한 Lean 4 형식화를 제공한다고 주장합니다. 그 의의는 다음과 같습니다:

1. 구체와 추상의 연결: "브리지 정리" 패턴은 mathlib4 의 추상 외미분에 대해 구체적인 좌표 구현을 검증하여 향후 형식화를 위한 재사용 가능한 방법론을 제공합니다.
2. 인프라 재사용: 이 개발은 기존 mathlib4 인프라 (발산 정리, extDeriv_pullback) 에 크게 의존하며, 고수준 라이브러리 구성 요소가 기초 분석을 재창조하지 않고 복잡한 기하학적 정리를 증명하는 데 어떻게 조립될 수 있는지를 보여줍니다.
3. 상호 보완성: 이 작업은 Harrison 의 HOL Light 형식화와 상호 보완적입니다. Harrison 이 게이지 적분을 사용하여 볼록/다면체 영역을 다루는 반면, 이 작업은 보흐너 적분과 mathlib4 의 미분 기하학 API 를 사용하여 매끄러운 특이 매개화를 다룹니다.
4. 기초 준비성: $\partial^2=0$ 을 증명하고 사슬 수준 스토크스 정리를 확립함으로써, 저자들은 mathlib4 의 다양체 적분 및 방향 API 가 성숙해지면 경계가 있는 매끄러운 다양체 위의 스토크스 정리에 대한 향후 완전한 형식화를 위한 필수적인 지역적 구성 요소를 제공합니다.

본 논문은 일반 다양체에서의 적분 문제를 해결하지는 않지만, 진정한 당김을 갖춘 중요한 "큐브-사슬" 계층을 확립하여 향후 확장을 위한 검증된 기초를 제공한다고 결론짓습니다.