Solutions of linear Cauchy–Riemann equations have no zeros near infinity

Proved

FiniteEnergyPlane.halfCyl_eventually_ne_zero

by Mazecto · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptotic-operatorpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S:\mathbb{R}^2\to\mathbb{R}^{2n\times2n}$ be $C^\infty$ and $1$ -periodic in $t$ , and $S_\infty$ a $C^\infty$ $1$ -periodic loop of symmetric matrices with $S\to S_\infty$ in $C^\infty$ . Let $\zeta$ be a solution of $\partial_s\zeta+J_0\partial_t\zeta+S\zeta=0$ on the half-cylinder, not identically zero on $(0,\infty)\times\mathbb{R}$ , with $\|\zeta(s,t)\|\le Ce^{\delta_0s}$ for $s>0$ . Then there is $s_0$ with $\zeta(s,t)\neq0$ for all $s\ge s_0$ and all $t$ .

Formalization Note No rate of convergence of $S$ and no nondegeneracy of $S_\infty$ is assumed.

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- A solution of `∂ₛζ + J₀ ∂ₜζ + S ζ = 0` on a half-cylinder, with `S(s, t) → S∞(t)` in `C^∞`,
not identically zero and with `‖ζ(s, t)‖ ≤ C e^{δ₀ s}`, has no zeros for `s` large. -/
theorem halfCyl_eventually_ne_zero {n : ℕ} (S : ℝ × ℝ → CauchyRiemannIndex.Mat n)
    (hS : ∀ i j, ContDiff ℝ ∞ (fun p : ℝ × ℝ => S p i j)) (hSper : ∀ s t : ℝ, S (s, t + 1) = S (s, t))
    (Sinf : ℝ → CauchyRiemannIndex.Mat n) (hSinf : CauchyRiemannIndex.IsSymLoop Sinf)
    (hSinf' : ∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j))
    (hSas : IsCInftyAsymptoticTo S Sinf)
    (ζ : ℝ × ℝ → CauchyRiemannIndex.Vec n) (hζ : IsHalfCylSolution S ζ)
    (hne : ∃ p : ℝ × ℝ, 0 < p.1 ∧ ζ p ≠ 0)
    (C δ₀ : ℝ) (hgrowth : ∀ s > 0, ∀ t : ℝ, ‖ζ (s, t)‖ ≤ C * Real.exp (δ₀ * s)) :
    ∃ s₀ : ℝ, ∀ s ≥ s₀, ∀ t : ℝ, ζ (s, t) ≠ 0 := by
  sorry

end FiniteEnergyPlane

Source

C. Wendl, Lectures on Symplectic Field Theory, lecture notes, Humboldt-Universität zu Berlin (2026 version); earlier version arXiv:1612.01009, Corollary 4.8.3

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `FiniteEnergyPlane.halfCyl_eventually_ne_zero`

Notation. $n \ge 0$ is an arbitrary natural number (including $n = 0$ ). $\mathrm{Mat}_n$ is the space of real $2n \times 2n$ matrices, rows and columns indexed by two copies of $\{0, \dots, n-1\}$ ; $\mathrm{Vec}_n = \mathbb{R}^{2n}$ with the Euclidean norm, indexed the same way. $J_0 \in \mathrm{Mat}_n$ is the block matrix $\begin{pmatrix} 0 & -I \\ I & 0 \end{pmatrix}$ . Matrices act on $\mathrm{Vec}_n$ by matrix–vector multiplication. For $\zeta : \mathbb{R}^2 \to \mathrm{Vec}_n$ , $\partial_s \zeta(s,t) = D\zeta(s,t)(1,0)$ and $\partial_t \zeta(s,t) = D\zeta(s,t)(0,1)$ (Fréchet derivative; $0$ where not differentiable). For matrix-valued or scalar $f : \mathbb{R}^2 \to F$ , $D^m f$ is the $m$ -th Fréchet derivative (operator norm, $\mathbb{R}^2$ with the max norm), and " $f \to 0$ in $C^\infty$ " means: $f$ is $C^\infty$ on $(s_0, \infty) \times \mathbb{R}$ for some $s_0$ , and for every $m \in \mathbb{N}$ and $\epsilon > 0$ there is $s_1$ with $\|D^m f(s,t)\| \le \epsilon$ for all $s \ge s_1$ , $t \in \mathbb{R}$ .

Data and hypotheses.

$S : \mathbb{R}^2 \to \mathrm{Mat}_n$ such that every entry $(s,t) \mapsto S(s,t)_{ij}$ is $C^\infty$ on $\mathbb{R}^2$ , and $S(s, t+1) = S(s, t)$ for all $s, t$ .
$S_\infty : \mathbb{R} \to \mathrm{Mat}_n$ which is continuous, $1$ -periodic, with $S_\infty(t)$ symmetric for every $t$ , and with every entry $t \mapsto S_\infty(t)_{ij}$ $C^\infty$ .
For every $i, j$ : $S(s,t)_{ij} - S_\infty(t)_{ij} \to 0$ in $C^\infty$ (as a function of $(s,t)$ , as $s \to +\infty$ ).
$\zeta : \mathbb{R}^2 \to \mathrm{Vec}_n$ is $C^\infty$ on $(0, \infty) \times \mathbb{R}$ , satisfies $\zeta(s, t+1) = \zeta(s, t)$ for all real $s, t$ , and

\partial_s \zeta(s,t) + J_0\, \partial_t \zeta(s,t) + S(s,t)\, \zeta(s,t) = 0 \qquad \text{for all } s > 0,\ t \in \mathbb{R}.

There is a point $(s,t)$ with $s > 0$ and $\zeta(s,t) \ne 0$ .
Real numbers $C$ and $\delta_0$ (no sign or size restriction) with $\|\zeta(s,t)\| \le C\, e^{\delta_0 s}$ for all $s > 0$ , $t \in \mathbb{R}$ . (Since the left side is $\ge 0$ , this hypothesis can only hold with $C \ge 0$ .)

Conclusion. There exists $s_0 \in \mathbb{R}$ such that $\zeta(s,t) \ne 0$ for every $s \ge s_0$ and every $t \in \mathbb{R}$ .

Remarks on edge cases. No nondegeneracy or invertibility assumption on $S_\infty$ (or on the operator $-J_0 \frac{d}{dt} - S_\infty$ ) is made. For $n = 0$ , $\mathrm{Vec}_0 = \{0\}$ , so the hypothesis that $\zeta$ is somewhere nonzero cannot hold and the statement is vacuous. The value of $s_0$ is not constrained (it need not be positive).

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Solutions of linear Cauchy–Riemann equations have no zeros near infinity

Read-back: FiniteEnergyPlane.halfCyl_eventually_ne_zero

Read-back: `FiniteEnergyPlane.halfCyl_eventually_ne_zero`