Sessão S3 · Esqueleto Lean 4 & AXLE Issue #12

§1 · Motivação

Por Que Lean 4, Por Que Agora

O Teorema 2.1 em sua forma simétrica é um resultado de EDO. O cálculo diz que é verdade. Então por que formalizar?

Transparência. A cadeia de Gronwall em S2 tinha meia dúzia de pequenas suposições ("assuma \(z(0) \geq \log 2\)", "use a hipótese de indução"). Em Lean 4 cada uma é uma obrigação separada e verificada por tipos.
Reúso. A cadeia de operadores \(G = U\circ F\circ K\circ C\) é uma afirmação estrutural sobre cada capítulo do GTCT. Uma formalização Lean 4 de \(G\) em uma situação (aqui: a EDO dm³) se torna um template para os outros capítulos.
Descoberta. Escrever a prova em Lean 4 foi o que expôs o AXLE Issue #12: a estimativa de Lipschitz que nosso artigo passa por cima. Lean não aceitou a passagem. Foi assim que a lacuna se tornou uma issue nomeada.

Nota Pedagógica

A formalização não é sobre certeza. É sobre localizar incerteza. A lacuna entre \(\varepsilon_0 = 1/3\) (Gronwall) e \(r_\star = 0{,}80\) (numérico) é uma lacuna matemática. O Issue #12 é uma lacuna formal — um lugar onde a prova Lean atualmente diz sorry. Ambas merecem atenção.

§2 · Leitura de Código

`AXLE/Chain.lean` — A Cadeia de Operadores

A cadeia de quatro operadores \(G = U\circ F\circ K\circ C\) do GTCT (contração, curvatura, filtro, desdobramento) é representada como uma structure dependente. Cada operador é um mapa entre espaços de estado com sua própria hipótese de regularidade.

Lean 4 · AXLE/Chain.lean
/- AXLE/Chain.lean — cadeia de operadores para GTCT -/import Mathlib.Analysis.ODE.Gronwall
import Mathlib.Analysis.NormedSpace.Basic
import Mathlib.Topology.MetricSpace.Lipschitz

namespaceAXLEstructureOperatorChain (α β γ δ ω : Type*)
    [MetricSpace α] [MetricSpace β] [MetricSpace γ]
    [MetricSpace δ] [MetricSpace ω] where
  C : α → β-- Contrair
  K : β → γ-- Curvatura
  F : γ → δ-- Filtrar
  U : δ → ω-- Desdobrar
  C_lip : LipschitzWith 1 C
  K_lip : ∃ L : ℝ≥0, LipschitzWith L K   -- ← Issue #12
  F_lip : LipschitzWith 1 F
  U_cont : Continuous U

defOperatorChain.compose
    (ch : OperatorChainα β γ δ ω) : α → ω :=
  ch.U ∘ ch.F ∘ ch.K ∘ ch.C

endAXLE

Lendo a estrutura

Note as hipóteses de regularidade: \(C\) e \(F\) são não-expansivas (LipschitzWith 1), \(U\) só precisa ser contínua (ela expande informação, não precisa preservar métrica), e \(K\) — o operador de curvatura, geometricamente o fluxo radial dm³ — carrega uma constante de Lipschitz existencial.

Nota de Design · Por que existencial para \(K\)

A constante de Lipschitz do fluxo radial dm³ em um dado instante depende da altura inicial \(z(0)\) e de \(\varepsilon\). Ela é limitada, mas o limite não é uniforme nos dados iniciais. Codificamos isso honestamente: \(K\) é Lipschitz, com alguma constante \(L\), e o resto da cadeia deve funcionar para qualquer tal \(L\). Isso é exatamente o que a API Lipschitz do Mathlib suporta.

§3 · O Teorema

`SpiralReturn` — Formalizando o Teorema 2.1

A EDO em si é uma aplicação de Picard–Lindelöf. O ODE.Gronwall e o ODE.PicardLindelof do Mathlib nos dão existência, unicidade e o lema de Gronwall. O esqueleto abaixo mostra o enunciado em sua forma atual.

Lean 4 · AXLE/SpiralReturn.lean
/- AXLE/SpiralReturn.lean — Teorema 2.1 (simétrico) -/import AXLE.Chain
import Mathlib.Analysis.ODE.PicardLindelof
import Mathlib.Analysis.SpecialFunctions.Log.Basic

namespaceAXLE/-- A equação radial dm³ em ε = 2. -/noncomputable defdm3Radial (z : ℝ) (r : ℝ) : ℝ :=
  r * (1 - r^2) + 2 * (r - 1) * Real.exp (-z)

/-- Teorema 2.1 (simétrico): se |r₀ - 1| < 1/3 e z₀ ≥ log 2,
    a solução converge exponencialmente para r = 1 à taxa -2. -/theoremspiralReturn
    {r₀ z₀ : ℝ}
    (hr : |r₀ - 1| < 1/3)
    (hz : z₀ ≥ Real.log 2) :
    ∃ (r : ℝ → ℝ), ∃ (μ : ℝ), μ < 0 ∧
      r 0 = r₀ ∧
      (∀ t ≥ 0, |r t - 1| ≤ |r₀ - 1| * Real.exp (μ * t)) := by-- Passo 1: aplica Picard–Lindelöf para existência local-- Passo 2: deriva a desigualdade escalar ½ d/dt u² ≤ (-2 + 3ε₀ + εe^{-z₀}) u²-- Passo 3: aplica Mathlib.Analysis.ODE.Gronwall-- Passo 4: a cota de Lipschitz necessária no Passo 2 — veja Issue #12sorryendAXLE

O que está provado, o que é `sorry`

Os Passos 1 e 3 do esboço de prova são chamadas de biblioteca. O ODE.PicardLindelof e o ODE.Gronwall do Mathlib são completos, mantidos e bem documentados. O Passo 2 — produzir a desigualdade escalar a partir da equação radial — precisa de uma cota no termo de acoplamento. Essa cota é o conteúdo do Issue #12.

Lema 2.1.A · A desigualdade escalar

Dados \(|u(0)| < 1/3\) e \(z(0) \geq \log 2\), existe \(\eta > 0\) tal que ao longo das soluções de dm³, \(\tfrac12 \frac{d}{dt} u^2 \leq -\eta\, u^2\) para todo \(t \geq 0\).

Isso é o que o Passo 2 deve entregar. Dado isso, o Passo 3 é uma aplicação de uma linha de Mathlib.Analysis.ODE.Gronwall. O \(\eta\) explícito é \(2 - 3\varepsilon_0 - 1 > 0\) quando \(\varepsilon_0 < 1/3\). O insumo ausente é uma cota de Lipschitz no acoplamento que é uniforme para todo \(t\) em que \(|u| < \varepsilon_0\). Isso é o Issue #12.

§4 · A Obrigação em Aberto

AXLE Issue #12 — A Estimativa de Lipschitz

#12 · Cota de Lipschitz no acoplamento \(\kappa(r,z) = \varepsilon(r-1)e^{-z}\) aberto · boa primeira issue

Objetivo: Provar kappa_lipschitz em AXLE/Coupling.lean:

Lean 4 · AXLE/Coupling.lean
lemmakappa_lipschitz
    (ε₀ : ℝ) (hε₀ : 0 < ε₀) (hε₀' : ε₀ < 1/3)
    (z_lo : ℝ) :
    ∃ L : ℝ≥0, ∀ r₁ r₂ : ℝ, ∀ z : ℝ,
      |r₁ - 1| < ε₀ → |r₂ - 1| < ε₀ → z ≥ z_lo →
      |κ r₁ z - κ r₂ z| ≤ L * |r₁ - r₂| := sorry

Dificuldade: Baixa — em forma de papel é uma estimativa de uma linha: \(\kappa\) é linear em \(r\) com inclinação \(\varepsilon e^{-z} \leq \varepsilon e^{-z_{\text{lo}}}\), então \(L = \varepsilon e^{-z_{\text{lo}}}\) funciona.

Por que está no Lean: Transformar essa estimativa de uma linha em Lean requer o Lipschitz.mk' correto, alguma plumagem NNReal para a constante, e cuidado com a monotonicidade de Real.exp. Um contribuidor Lean iniciante pode fazer em uma tarde.

Caminho de contribuição

git clone https://github.com/TOTOGT/AXLE
Abra AXLE/Coupling.lean no VS Code com a extensão Lean 4.
Substitua o sorry por um termo de prova real.
lake build para verificar tipos; abra um PR.

Relacionado: duas issues já fechadas

#8 · Portar dm3Radial para a forma de ODE.Gronwall.comparison fechado · merged #11

Reescrever a desigualdade escalar na forma que o lema de comparação de Gronwall do Mathlib espera (\(\dot u \leq f(u)\) com \(f\) localmente Lipschitz). Feito — levou duas rodadas de revisão.

#9 · Positividade de \(\{r > 1\}\) (o exercício de quadro de S1) fechado · merged #10

Formalizar o exercício de quadro de S1: \(\{r(t) > 1\}\) é positivamente invariante. Feito via Mathlib.Analysis.ODE.Invariant.

Além do #12. A bacia precisa \(r_\star \approx 0{,}80\) é um projeto de pesquisa separado, não uma lacuna de formalização. Nenhuma quantidade de Lean vai afiar \(1/3\) para \(0{,}80\) — isso requer um argumento matemático novo, provavelmente uma função de Lyapunov com estrutura sensível ao sinal. Se quiser trabalhar nisso, o laboratório numérico (labs/dm3_numeric.py) é o lugar para começar.

§5 · Simulador de Referência

▶ Fluxo dm³ — Referência

Mantenha este aberto enquanto lê o Lean. As órbitas que você vê são exatamente o que spiralReturn promete — módulo Issue #12.

▶ Fluxo de Contato dm³ — O que spiralReturn promete, visualizado

§6 · Fechamento

O Que o Curso Fez

Em três horas caminhamos de variedades de contato em dimensão 3 (S1) por Teorema 2.1 com sua bacia de Gronwall (S2) até uma formalização Lean 4 com uma obrigação em aberto (S3). A formalização está viva, pública e recebe contribuições. A bacia precisa \(r_\star\) é pesquisa aberta. O simulador dm³ roda em qualquer navegador.

Se você contribuir uma prova de kappa_lipschitz, você fecha o último sorry na prova simétrica do Teorema 2.1. A cadeia de operadores \(G = U\circ F\circ K\circ C\) então terá uma instância completamente verificada. Isso é um marco: um teorema GTCT com prova verificada por máquina.

Conclusão Final · O mapa do território

A geometria (S1) força uma hélice. A forma de contato não é decoração; é o suporte de \(\Gamma\).
A análise (S2) prova contração exponencial à taxa \(-2\), numa bola de Gronwall \(|r - 1| < 1/3\).
A numeração (S2) corrige a fronteira interior para \(r_\star \approx 0{,}80\) — mais restritiva que Gronwall, não mais fraca.
A formalização (S3) reduz o teorema simétrico inteiro a um lema estilo Mathlib: kappa_lipschitz.

Quatro camadas, quatro contribuições, uma hélice. Obrigado, Natal.

Rampa de Contribuição · Três Horizontes de Tempo

Curto prazo (tarde). Feche o Issue #12. Baixa dificuldade, alta clareza, atribuição nomeada no log de commits do AXLE.
Médio prazo (semana). Formalize o Corolário 2.3 (a bacia explícita) como consumidor de spiralReturn. Depende do #12 estar fechado.
Longo prazo (pesquisa). Encontre a função de Lyapunov sensível ao sinal que produz \(r_\star\). Isso é um artigo, não uma issue.

← Sessão Anterior

S2: Teorema 2.1 & a Bacia Assimétrica

Retornar ao Hub →

Vol. IV · Atratores Helicoidais