Teorema 2.1 — Contração Exponencial a \(\Gamma\)
Recordamos o sistema dm³ de S1 com acoplamento fixo \(\varepsilon = 2\):
Existe \(\varepsilon_0 > 0\) tal que toda solução com \(|r(0) - 1| < \varepsilon_0\) satisfaz
\[\limsup_{t\to\infty} \frac{1}{t}\,\log|r(t) - 1| \;\leq\; -2,\]e consequentemente \(r(t) \to 1\), \(z(t)/t \to 1\), \(\theta(t) - t \to \text{const}\); i.e. a trajetória converge para a hélice \(\Gamma = \{r = 1\}\) à taxa exatamente \(e^{-2t}\). O argumento elementar de Gronwall fornece \(\varepsilon_0 = 1/3\).
Leia o teorema com atenção: a taxa \(\mu = -2\) é precisa — é o autovalor Jacobiano, não uma cota de Lyapunov. A bacia \(\varepsilon_0\) é onde o problema vive.
Linearização em \(r = 1\)
Ponha \(u = r - 1\) e expanda a equação radial. Em \(r = 1\) o acoplamento se anula identicamente, então até primeira ordem o termo \(\varepsilon\) não contribui para a parte linear. O termo de Hopf: \(r(1-r^2) = -2u + O(u^2)\). Portanto:
A contribuição linear-em-\(u\) do acoplamento \(\varepsilon(r-1)e^{-z} = \varepsilon\,u\,e^{-z}\) é explícita: carrega um fator \(e^{-z(t)}\). Como \(\dot z \to 1\) ao longo de qualquer órbita próxima, \(z(t) \to +\infty\) e \(e^{-z(t)} \to 0\). A parte linear de acoplamento é uma perturbação decadente da taxa estrita \(-2\).
Linearizando o sistema completo em qualquer ponto \((\theta, z)\) do ciclo limite \(\Gamma = \{r=1\}\) obtemos um Jacobiano bloco-triangular cujo autovalor radial é \(\mu = \partial_r\,\dot r \big|_{r=1} = 1 - 3r^2 + \varepsilon\,e^{-z}\big|_{r=1} = -2 + \varepsilon\,e^{-z}\). Quando \(z\to\infty\) a perturbação some e o autovalor tende a \(-2\). É por isso que toda trajetória numérica na Tabela 1 lerá um \(\hat\mu\) perto mas levemente menos negativo que \(-2\).
De onde vem \(-2\) em uma linha?
De \(\tfrac{d}{dr}\bigl[r - r^3\bigr]_{r=1} = 1 - 3 = -2\). A forma normal de Hopf sozinha entrega a taxa. O acoplamento de contato não a altera. Todo outro termo no sistema é ordem superior em \(u\) ou suprimido por \(e^{-z}\).
O Esboço de Gronwall
Queremos uma bacia não-linear e explícita — o conjunto de \(r(0)\) iniciais para os quais podemos provar que \(r(t) \to 1\). O caminho mais limpo é um argumento de Gronwall estilo energia em \(u = r - 1\).
Passo 1. A desigualdade escalar.
Multiplique a equação radial por \(u\) e expanda \(r(1-r^2) = -2u - 3u^2 - u^3\). Obtém-se:
Os termos perigosos para análise de \(u\) pequeno são \(-3u^3\) (que pode mudar de sinal) e o termo \(\varepsilon\) (positivo e que só decai com \(z\)). Guardamos o resto como \(-2u^2 - u^4 \leq -2u^2\).
Passo 2. Cote as partes ruins.
Assuma \(|u(0)| < \varepsilon_0\) e, como hipótese de indução, \(|u(t)| < \varepsilon_0\) para todo \(t\) considerado. Então \(|3u^3| \leq 3\varepsilon_0 u^2\). Agrupando:
Passo 3. Resolva para \(\varepsilon_0\).
Para \(\varepsilon = 2\) fixo e \(z(0) \geq 0\), o fator exponencial é no máximo \(1\). Pinçando em \(z(0) \geq \log\varepsilon = \log 2\) reduz a cota a:
O número \(1/3\) é um artefato algébrico da estimativa de Gronwall. É o que a cota de valor absoluto do pior caso permite. Trata \(+u\) e \(-u\) de forma idêntica — uma simetria que a EDO original não respeita.
Se \(|r(0) - 1| < 1/3\) então \(r(t) \to 1\) exponencialmente. Em particular, qualquer \(r(0) \in (2/3,\, 4/3)\) está na bacia de atração de \(\Gamma\), e \(|r(t) - 1| \leq |r(0)-1|\,e^{\mu t}\) para algum \(\mu \leq -\eta < 0\).
Tabela 1 — DOP853 @ rtol \(10^{-10}\), atol \(10^{-12}\)
Integramos (1) com \(\theta(0) = 0\), \(z(0) = 0\), e variamos \(r(0)\). Para cada execução registramos a taxa de contração empírica \(\hat\mu\), definida como a inclinação de \(\log|r(t) - 1|\) em \(t \in [5, 20]\).
| \(r(0) - 1\) | \(\hat\mu\) (exterior) | \(r(0)\) | \(\min_{t\le 30} \dot z\) | resultado |
|---|---|---|---|---|
| \(+0{,}10\) | \(-1{,}849\) | \(0{,}90\) | \(+0{,}15\) | converge |
| \(+0{,}33\) | \(-1{,}890\) | \(0{,}80\) | \(-0{,}02\) | limiar · borda da bacia |
| \(+0{,}50\) | \(-1{,}907\) | \(0{,}70\) | \(-0{,}18\) | colapsa |
| \(+1{,}00\) | \(-1{,}932\) | \(0{,}50\) | \(-0{,}48\) | colapsa |
| \(+1{,}50\) | \(-1{,}959\) | \(0{,}30\) | \(-0{,}93\) | colapsa |
Lendo a tabela.
- Coluna exterior. Todo \(r(0) > 1\) converge. \(\hat\mu\) é próximo de \(-2\) e se aproxima monotonicamente de baixo à medida que \(r(0) - 1\) cresce. Nenhum valor até \(1{,}5\) se comporta mal.
- Coluna interior. \(r(0) = 0{,}90\) converge. \(r(0) = 0{,}80\) está na borda — \(\dot z\) frisa zero mas a órbita sobrevive. Abaixo de \(r(0) = 0{,}80\) a trajetória cai verticalmente (\(\dot z\) negativo), \(e^{-z}\) explode, o acoplamento domina, e \(r\) abandona toda vizinhança de \(1\) em tempo finito.
Gronwall disse \(r(0) \in (2/3,\, 4/3) = (0{,}667,\, 1{,}333)\). A realidade diz \(r(0) \in (0{,}80,\, +\infty)\). A fronteira exterior de Gronwall é vácua — não há fronteira exterior nessa janela. A fronteira interior está em \(r_\star \approx 0{,}80\), mais restritiva que o palpite de Gronwall de \(2/3 \approx 0{,}667\). Gronwall teria declarado \(r(0) = 0{,}70\) seguro; DOP853 diz que colapsa.
O que dá errado geometricamente
Em \(r(0) < 1\), o termo de Hopf \(r(1-r^2)\) empurra \(r\) para cima, bom. Mas o acoplamento de contato \(\varepsilon(r-1)e^{-z}\) tem sinal oposto — e pior, quando \(r < 1\) a equação vertical adquire uma contribuição negativa \(-\varepsilon(r-1)^2 e^{-z}\). Se \(r\) começa muito pequeno, \(\dot z\) pode ser dominado; \(z\) cai; \(e^{-z}\) explode; o acoplamento fica descontrolado. O termo de Hopf, limitado próximo de \(r=1\), não consegue nos salvar.
Demo Numérica ao Vivo
Demo guiada (8 min)
- \(r_0 = 0{,}90\), \(\varepsilon = 2\). Espiral limpa subindo para \(r = 1\). Observe cor ficar azul.
- \(r_0 = 0{,}80\). Trajetória achata; há um momento visível onde a órbita paira. Cor muda para dourado e recupera.
- \(r_0 = 0{,}70\). Trajetória cai abaixo do anel \(r = 0{,}80\) (dourado) e fica vermelha. A leitura de \(z\) começa a diminuir.
- \(r_0 = 1{,}50\) para contraste. Converge rápido. A bacia exterior não tem problemas.
Transição para a Sessão S3
Temos agora dois números em tensão:
- \(\varepsilon_0 = 1/3\) — o que a desigualdade de Gronwall do livro-texto permite;
- \(r_\star \approx 0{,}80\) — o que o fluxo real faz.
Em S3 traduzimos a prova do Teorema 2.1 — a versão simétrica — para Lean 4 / Mathlib 4. O esqueleto formal está no AXLE (Chain.lean, SpiralReturn). A obrigação aberta é a estimativa de Lipschitz do acoplamento, rastreada como AXLE Issue #12.
Mostre que Gronwall não pode dar \(\varepsilon_0 > 1/3\) para esta forma da estimativa.
Fixe \(\varepsilon = 2\), \(z(0) \geq \log 2\). Argumente que a desigualdade \(-2 + 3\varepsilon_0 + 1 < 0\) é apertada — os coeficientes \(2, 3, 1\) são exatamente o que \(r(1-r^2)\) e o acoplamento produzem; não há folga para recuperar. Conclua: qualquer melhora deve mudar a estimativa, não ajustar suas constantes. É precisamente por isso que a fronteira interna precisa \(r_\star\) requer uma técnica de prova diferente — uma sensível ao sinal, não apenas à magnitude.
A cota de Gronwall não está errada. Ela é grosseira. Uma cota grosseira é uma perda de informação. Localizar essa informação — o que uma estimativa com sinal poderia capturar que uma de valor absoluto não pode — é trabalho em aberto.