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

Resumo Técnico: Teorema de Stokes para Cubos Singulares Suaves em Lean 4

Enunciado do Problema
Até abril de 2026, o ecossistema Lean 4 (especificamente mathlib4) carecia de uma formalização completa do teorema de Stokes para formas diferenciais em variedades suaves com bordo ou para cadeias singulares. Embora o mathlib4 possuísse o teorema da divergência para caixas alinhadas aos eixos e uma derivada exterior abstrata (extDeriv), ainda não fornecia um teorema que integrasse o pullback de uma forma diferencial sobre um cubo singular suave (um mapa suave de um cubo unitário para um espaço euclidiano arbitrário) e o igualasse à soma alternada de integrais sobre as faces do bordo. Formalizações existentes, como o trabalho de Harrison no HOL Light, cobriam domínios convexos e poliedrais, mas não abordavam parametrizações singulares suaves ou a infraestrutura específica da álgebra exterior abstrata do mathlib4.

Metodologia
Os autores apresentam uma formalização "sem sorry" (zero suposições não provadas) que preenche a lacuna entre a integração baseada em coordenadas e a geometria diferencial abstrata. O desenvolvimento baseia-se em três pilares metodológicos principais:

1. Pullback Verdadeiro via Derivada de Fréchet: A construção central define o pullback de uma forma diferencial $\sigma^*\omega$ usando a derivada de Fréchet ($fderiv$) de um mapa globalmente $C^\infty$ $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$. Diferentemente da simples pré-composição de coeficientes, esta definição aplica a forma no ponto imagem $\sigma(x)$ a vetores empurrados para frente por $D\sigma(x)$, aderindo às definições padrão da geometria diferencial.
2. Redução ao Teorema de Stokes para Caixas: A estratégia de prova reduz o caso singular ao caso de caixas alinhadas aos eixos. Ao aproveitar o teorema extDeriv_pullback do mathlib4, os autores estabelecem a identidade de naturalidade $d(\sigma^*\omega) = \sigma^*(d\omega)$. Isso permite a aplicação do teorema de Stokes existente para caixas (derivado do teorema da divergência do mathlib4) à forma puxada para trás $\sigma^*\omega$ sobre o domínio de parâmetros $[0,1]^{n+1}$.
3. Correspondência de Faces e Álgebra em Nível de Cadeia: Um componente técnico crítico é a "identidade de correspondência de faces", que prova que a integral da forma puxada para trás sobre uma face do bordo de uma caixa corresponde exatamente à integral da forma sobre a face singular correspondente. Além disso, os autores formalizam a identidade do complexo de cadeias $\partial(\partial\sigma) = 0$ para cadeias singulares. Isso é alcançado não definindo um homomorfismo de bordo em caixas não decoradas, mas construindo uma involução que inverte sinais e não possui pontos fixos no conjunto de índices do dobro-bordo, provando que os termos pareados se cancelam algebricamente.

Contribuições Principais
O artigo entrega uma formalização abrangente composta por 44 módulos Lean (aproximadamente 4.000 linhas) com 205 declarações nomeadas. As contribuições específicas incluem:

• Teorema de Stokes Singular: Um teorema afirmando que, para qualquer mapa globalmente $C^\infty$ $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ e qualquer $n$-forma $C^\infty$ $\omega$, a integral de $\sigma^*(d\omega)$ sobre o cubo unitário é igual à soma alternada das integrais de $\sigma^*\omega$ sobre as $2(n+1)$ faces.
• Teorema de Ponte: Uma prova formal que valida que a derivada exterior baseada em coordenadas dos autores (extDerivCoord) é consistente com a extDeriv abstrata do mathlib4 quando avaliada em vetores da base padrão. Isso garante que a implementação baseada em coordenadas é matematicamente sólida em relação à API abstrata da biblioteca.
• Extensões em Nível de Cadeia: A extensão do teorema de Stokes para combinações lineares formais $\mathbb{Z}$ de cubos singulares (cadeias singulares) via linearidade.
• Prova de $\partial^2 = 0$: Uma prova formal da identidade do complexo de cadeias $\partial(\partial\sigma) = 0$ para cadeias singulares, utilizando uma involução combinatória no conjunto de índices das duplas faces.
• Especializações Dimensionais: Instanciações diretas do teorema principal recuperando o Teorema Fundamental do Cálculo (FTC), o Teorema de Green, o Teorema da Divergência e o Teorema de Gauss 3D, bem como integração por partes e a regra de Leibniz.
• Auditoria de Axiomas: Verificação de que todo o desenvolvimento depende apenas dos três axiomas padrão do Lean 4 (propext, Classical.choice, Quot.sound), confirmado por meio de 79 verificações sistemáticas #print axioms.

Resultados e Escopo
A formalização prova com sucesso o teorema de Stokes para:

1. Cubos Singulares Suaves: Mapas $\sigma$ que são globalmente suaves em $\mathbb{R}^{n+1}$, integrados sobre o cubo de parâmetros $[0,1]^{n+1}$.
2. Caixas Alinhadas aos Eixos: $n$-formas coordenadas em caixas $[a,b] \subset \mathbb{R}^{n+1}$.

O artigo observa explicitamente as seguintes limitações e fronteiras de escopo:

• Sem Teoria de Variedades: O domínio de integração é estritamente o cubo de parâmetros ou uma caixa. O trabalho não formaliza a integração sobre variedades suaves gerais, nem utiliza partições da unidade, cartas ou atlas.
• Suavidade Global: Os mapas singulares são exigidos para serem $C^\infty$ em todo $\mathbb{R}^{n+1}$, uma condição mais forte do que a suavidade apenas no cubo fechado. Essa escolha foi feita para simplificar a formalização, evitando argumentos de regularidade de bordo e garantindo que a derivada de Fréchet esteja bem definida em todos os lugares.
• Sem Semântica de Domínio Imagem: O teorema trata a integral como uma operação sobre o domínio de parâmetros. Não prova que a imagem de $\sigma$ constitui uma subvariedade ou uma cadeia geométrica orientada no espaço alvo.

Significado e Alegações
Os autores afirmam que este trabalho fornece a primeira formalização completa em Lean 4 do teorema de Stokes para cubos singulares suaves com um pullback de "verdadeira" forma diferencial. Seu significado reside em:

1. Ponte entre Concreto e Abstrato: O padrão do "teorema de ponte" valida uma implementação concreta baseada em coordenadas contra a derivada exterior abstrata do mathlib4, oferecendo uma metodologia reutilizável para futuras formalizações.
2. Reutilização de Infraestrutura: O desenvolvimento depende fortemente da infraestrutura existente do mathlib4 (teorema da divergência, extDeriv_pullback), demonstrando como componentes de alto nível da biblioteca podem ser compostos para provar teoremas geométricos complexos sem reinventar a análise fundamental.
3. Complementaridade: O trabalho é complementar à formalização em HOL Light de Harrison. Enquanto Harrison cobre domínios convexos/poliedrais com integração de gauge, este trabalho cobre parametrizações singulares suaves usando integração de Bochner e a API de geometria diferencial do mathlib4.
4. Preparação Fundamental: Ao provar $\partial^2=0$ e estabelecer o teorema de Stokes em nível de cadeia, os autores fornecem um bloco de construção local necessário para uma futura formalização completa do teorema de Stokes em variedades suaves com bordo, assim que as APIs de integração e orientação de variedades do mathlib4 amadurecerem.

O artigo conclui que, embora não resolva o problema da integração em variedades gerais, ele estabelece a camada crítica de "cadeia-cúbica" com pullbacks verdadeiros, servindo como uma fundação verificada para futuras extensões.