The fundamental solution of a symmetric loop is symplectic

Proved

AsymptoticOperator.fundamentalSolution_symplectic

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

asymptotic-operatorconley-zehnder-indexspectral-theorysymplectic-geometryunbounded-operator

Let $S:S^1\to\mathbb{R}^{2n\times2n}$ be continuous with $S(t)^{\mathsf T}=S(t)$ for all $t$ , and let $\Psi$ be its fundamental solution. Then $\Psi(t)\in\mathrm{Sp}(2n)$ , i.e. $\Psi(t)J_0\Psi(t)^{\mathsf T}=J_0$ , for every $t\in\mathbb{R}$ .

Preamble

import Definitions.Def_AsymptoticOperator_Setting

Formal statement

namespace AsymptoticOperator

open ConleyZehnder

/-- Wendl §3.4, p. 61: for a loop of symmetric matrices the fundamental solution is a path
in `Sp(2n)` starting at `Id`. -/
theorem fundamentalSolution_symplectic {n : ℕ} (S : C(UnitAddCircle, Mat n))
    (hS : IsSymLoop S) (Ψ : ℝ → Mat n) (hΨ : IsFundamentalSolution S Ψ) (t : ℝ) :
    IsSymplectic (Ψ t) := by sorry

end AsymptoticOperator

Source

Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, §3.4, p. 61 (informal there)

Read-back

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

Setting. Let $n \ge 0$ be a natural number (the case $n = 0$ is included; then all matrices below are $0 \times 0$ and every condition is trivially true). Write $\mathrm{Mat}_n$ for the real $2n \times 2n$ matrices, with rows and columns indexed by two disjoint copies of $\{0,\dots,n-1\}$ (a "first block" and a "second block"). Let

J_0 = \begin{pmatrix} 0 & -I_n \\ I_n & 0 \end{pmatrix} \in \mathrm{Mat}_n .

A matrix $A \in \mathrm{Mat}_n$ is called symplectic if

A\, J_0\, A^{\mathsf T} = J_0 .

Let $S^1 = \mathbb{R}/\mathbb{Z}$ . For $t \in \mathbb{R}$ , $S(t)$ means $S$ evaluated at the class $t \bmod 1$ .

Hypotheses.

$S : \mathbb{R}/\mathbb{Z} \to \mathrm{Mat}_n$ is continuous (entrywise topology).
$S$ is a loop of symmetric matrices: $S(t)^{\mathsf T} = S(t)$ for every $t \in \mathbb{R}/\mathbb{Z}$ .
$\Psi : \mathbb{R} \to \mathrm{Mat}_n$ is a fundamental solution of $S$ , meaning: $\Psi(0) = I_{2n}$ , and for every $t \in \mathbb{R}$ , $\Psi$ is differentiable at $t$ (as a map into $\mathrm{Mat}_n$ with its entrywise/finite-dimensional topology) with derivative $\Psi'(t) = J_0\, S(t)\, \Psi(t)$ (matrix products in this order).
$t \in \mathbb{R}$ is arbitrary (any real number, not only $t \in [0,1]$ ).

Conclusion. $\Psi(t)$ is symplectic:

\Psi(t)\, J_0\, \Psi(t)^{\mathsf T} = J_0 .

In words: for every continuous $1$ -periodic loop of real symmetric $2n\times 2n$ matrices $S$ , every function $\Psi$ with $\Psi(0) = I$ and $\Psi' = J_0 S \Psi$ everywhere on $\mathbb{R}$ satisfies $\Psi(t) J_0 \Psi(t)^{\mathsf T} = J_0$ for all real $t$ .

Human review

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

View graph