Symplectic geometry and topology

The state of a mechanical system with $n$ degrees of freedom is a point $(q, p)$ of phase space: $n$ positions and $n$ momenta. Its motion is the flow of Hamilton's equations

where $H$ is the energy. In 1838 Liouville observed that this flow preserves volume: a blob of initial conditions may be stretched into a long filament, but its $2n$-dimensional volume never changes. Statistical mechanics is built on that fact.

Is volume all that a Hamiltonian flow remembers? In 1985 Mikhail Gromov showed that it is not. Take the round ball $B^{2n}(r)$ of radius $r$ and the cylinder $Z(R) = \{x_1^2 + y_1^2 \le R^2\} \subset \R^{2n}$, built on one pair of conjugate coordinates. If $n \ge 2$ the cylinder has infinite volume, so there is plenty of room, and indeed a volume-preserving linear map — $(x_1, y_1, x_2, y_2) \mapsto (\varepsilon x_1, \varepsilon y_1, x_2/\varepsilon, y_2/\varepsilon)$ — puts the ball inside an arbitrarily thin cylinder. But no Hamiltonian flow, and no symplectic map at all, can put $B^{2n}(r)$ inside $Z(R)$ unless $r \le R$. A Hamiltonian system cannot squeeze a cloud of states through a hole in a conjugate plane smaller than the cloud's own cross-section. (The result is often called "the symplectic camel", after the camel and the eye of the needle.)

This lesson is an orientation to the geometry behind that rigidity. Its paradox is the subject in miniature: symplectic manifolds have no local invariants whatsoever (Darboux's theorem), yet they carry deep global invariants, detected by holomorphic curves and Floer homology, that see far more than volume.

The symplectic form of $\R^{2n}$ is

Evaluated on two vectors $u, v$ it gives $\omega_0(u, v) = \sum_i (u_{x_i} v_{y_i} - u_{y_i} v_{x_i})$: the sum of the signed areas of the shadows of the parallelogram spanned by $u$ and $v$ on the $n$ conjugate planes $(x_i, y_i)$. A map that preserves $\omega_0$ preserves the total oriented area of every small piece of surface, measured plane by plane.

• In dimension $2$ this is just area (and orientation). There symplectic and area-preserving mean the same thing.
• In dimension $2n \ge 4$ preserving $\omega_0$ is far stronger than preserving volume, which is $\omega_0^n / n!$. The squeeze above preserves volume but multiplies the area of the $(x_1, y_1)$-shadow by $\varepsilon^2$.

Hamilton's equations say $\dot z = J \nabla H$ with $J = \left(\begin{smallmatrix} 0 & I \\ -I & 0 \end{smallmatrix}\right)$ in the coordinates $(q, p)$: the flow moves perpendicular to the gradient of $H$, rotated by a quarter turn in each conjugate plane. Moving perpendicular to $\nabla H$ keeps $H$ constant; rotating by $J$ is what preserves area.

Prerequisites are smooth manifolds, differential forms (Cartan's formula $\mathcal{L}_X = d\iota_X + \iota_X d$ in particular) and the Hamiltonian side of classical mechanics.

Evenness also has a one-line matrix proof, which is the one formalised below: the Gram matrix $\Omega$ of $\omega$ is skew-symmetric, so $\det \Omega = \det \Omega^{\mathsf T} = \det(-\Omega) = (-1)^{\dim V} \det \Omega$, and if $\dim V$ is odd then $\det \Omega = 0$.

In a Darboux basis $\omega^n = n!\, e_1^* \wedge f_1^* \wedge \dots \wedge e_n^* \wedge f_n^* \neq 0$, and conversely $\omega^n \neq 0$ forces non-degeneracy. So on a symplectic manifold $\omega^n / n!$ is a volume form, the Liouville volume, and every symplectic manifold is orientable.

For $n = 1$, $\operatorname{Sp}(2, \R) = SL(2, \R)$: a $2 \times 2$ matrix satisfies $A^{\mathsf T} J A = (\det A)\, J$, so it is symplectic exactly when $\det A = 1$. In general every symplectic matrix has determinant $1$ (linear Liouville; this needs an argument, since $A^{\mathsf T} J A = J$ only gives $(\det A)^2 = 1$), and $\operatorname{Sp}(2n, \R) \cap O(2n) = U(n)$.

The volume-preserving squeeze of the motivation fails the hypothesis: it multiplies $\omega_0(e_{x_1}, e_{y_1})$ by $\varepsilon^2$. Gromov's theorem below says that Theorem 3 survives for non-linear symplectic embeddings — which is astonishing, because Darboux's theorem says there is no local obstruction of any kind.

Note what each part uses: (i) only that $\omega$ is alternating, (ii) that $\omega$ is closed, and the existence of $X_H$ that $\omega$ is non-degenerate. Part (i) is formalised below in exactly this generality.

Two consequences are worth stating. Noether's theorem: $\{F, H\} = 0$ means both that $F$ is conserved by the flow of $H$ and that $H$ is conserved by the flow of $F$ — a symmetry and a conserved quantity are the same thing. Symplectic versus Hamiltonian: a vector field $X$ with $\mathcal{L}_X \omega = 0$ has $\iota_X \omega$ closed; it is Hamiltonian exactly when $\iota_X \omega$ is exact. So $H^1_{dR}(M)$ measures the difference, as the translation of $T^2$ showed.

At the linear level, a quadratic Hamiltonian $H(z) = \frac12 z^{\mathsf T} S z$ ($S$ symmetric) has $X_H(z) = JSz$, and Liouville's theorem becomes $\operatorname{tr}(JS) = 0$: indeed $\operatorname{tr}(JS) = \operatorname{tr}((JS)^{\mathsf T}) = \operatorname{tr}(S^{\mathsf T} J^{\mathsf T}) = -\operatorname{tr}(SJ) = -\operatorname{tr}(JS)$, so $\det e^{tJS} = e^{t \operatorname{tr}(JS)} = 1$.

Moser's trick (1965) turns "find a diffeomorphism pulling one form back to another" into "solve a linear equation for a vector field", which non-degeneracy makes trivial.

No local invariants. In Riemannian geometry the curvature tensor is a local invariant: by Gauss's Theorema Egregium no piece of a round sphere is isometric to a piece of the plane (see Riemannian geometry). Darboux's theorem says every symplectic manifold of dimension $2n$ looks locally exactly like $(\R^{2n}, \omega_0)$: symplectic geometry is, locally, as flexible as topology. Moser's method gives global versions too: two area forms on a closed connected surface with the same total area differ by a diffeomorphism, and (Weinstein, 1971) a neighbourhood of a Lagrangian submanifold $L$ is symplectomorphic to a neighbourhood of the zero section in $T^*L$.

Gromov's non-squeezing theorem (1985). If $B^{2n}(r)$ embeds symplectically into $Z(R) = B^2(R) \times \R^{2n-2}$, then $r \le R$. This is a theorem, proved with pseudo-holomorphic curves, which Gromov introduced in the same paper. Sketch: choose an almost complex structure $J$ on $M = S^2 \times T^{2n-2}$ (with $S^2$ of area slightly more than $\pi R^2$, containing $B^2(R)$, and a large torus) that is tamed by the symplectic form and equals the push-forward of the standard complex structure on the image of the ball. Gromov proves that for every tamed $J$, through every point passes a $J$-holomorphic sphere in the class $[S^2 \times \mathrm{pt}]$ — the count of such spheres is a deformation invariant equal to $1$. The sphere through the image of the centre has symplectic area $\pi R^2 + \varepsilon$. Pulled back to the ball it becomes a genuine holomorphic curve through the centre, hence a minimal surface, and the monotonicity formula for minimal surfaces gives it area at least $\pi r^2$ inside the ball. So $\pi r^2 \le \pi R^2 + \varepsilon$ for every $\varepsilon > 0$. What is proved in this lesson is the linear case (Theorem 3), which needs none of this machinery.

Capacities and $C^0$-rigidity. Ekeland–Hofer (1989) and Hofer–Zehnder (1990) axiomatised the invariant behind non-squeezing: a symplectic capacity assigns to each symplectic manifold of dimension $2n$ a number $c(M) \in [0, \infty]$, monotone under symplectic embeddings, scaling like $c(M, \lambda\omega) = \lambda\, c(M, \omega)$ and normalised by $c(B^{2n}(1)) = c(Z(1)) = \pi$. Gromov's width $\sup\{\pi r^2 : B(r) \hookrightarrow M\}$ is the smallest one. Capacities are $C^0$-robust, and they give the Eliashberg–Gromov theorem: a diffeomorphism that is a $C^0$-limit of symplectomorphisms is itself symplectic. Volume preservation would not have predicted this.

The Arnold conjecture. Let $(M, \omega)$ be closed and $\varphi \in \operatorname{Ham}(M, \omega)$ have only non-degenerate fixed points ($\det(d\varphi_x - I) \neq 0$). Arnold conjectured in the 1960s that

the number of critical points that a Morse function on $M$ is forced to have by Morse theory. Compare the Lefschetz fixed-point theorem, which only bounds the signed count, by $\chi(M)$; for the torus $T^{2n}$, $\chi = 0$ gives nothing, while the Arnold bound is $2^{2n}$. And the Hamiltonian hypothesis is essential: translations of $T^2$ are symplectic and have no fixed points at all.

What is proved, and what is open:

• Proved. Conley–Zehnder (1983) for the torus $T^{2n}$; Floer (1987–89) for monotone and symplectically aspherical manifolds, with $\mathbb{F} = \Z/2$; for all closed symplectic manifolds with $\mathbb{F} = \Q$ by Fukaya–Ono and by Liu–Tian (both 1998–99), using "virtual" counts of holomorphic curves; Abouzaid and Blumberg (2021) extended the bound to coefficients in every finite field.
• Open in general. Arnold's original, stronger form, with the minimal number of critical points of any smooth function on $M$ in place of the sum of Betti numbers; and the version for degenerate fixed points (a lower bound by the cup-length plus one), which is known only in special cases such as symplectically aspherical manifolds.

Floer homology: Morse theory on the loop space. Floer's idea was to do Morse theory for the action functional on the space of contractible loops $\gamma : S^1 \to M$,

(signs vary with conventions). Its critical points are the $1$-periodic orbits of $X_{H_t}$, which correspond to fixed points of $\varphi = \varphi^1_H$. With a compatible almost complex structure $J$, its "gradient flow lines" are maps $u : \R \times S^1 \to M$ solving Floer's equation

a perturbed Cauchy–Riemann equation. The functional is not bounded and its Hessian has infinite index in both directions, so classical Morse theory fails; but solutions of finite energy behave like holomorphic curves. Counting the rigid solutions defines a differential on the vector space generated by the periodic orbits. Its homology $HF_*(H)$ does not depend on $H$ or $J$, and for a small time-independent Morse function it equals the Morse homology of $M$, which is $H_*(M)$. Since a chain complex has at least as many generators as the rank of its homology, $\#\operatorname{Fix}(\varphi) \ge \operatorname{rank} H_*(M)$. The analytic difficulties — transversality, and the bubbling-off of holomorphic spheres in the compactness theorem — are exactly why the monotone case came first and the general case needed virtual techniques.

Moment maps. If a torus $T$ acts on $(M, \omega)$ by symplectomorphisms generated by Hamiltonians, these assemble into a moment map $\mu : M \to \mathfrak{t}^*$ with $d\langle \mu, \xi \rangle = \iota_{\xi_M} \omega$ for every $\xi \in \mathfrak{t}$. For the rotation of $S^2$ the moment map is the height. Established landmarks:

• Convexity (Atiyah; Guillemin–Sternberg, 1982): for a compact connected $M$, $\mu(M)$ is the convex hull of the images of the fixed points — a convex polytope.
• Delzant (1988): compact symplectic $2n$-manifolds with an effective Hamiltonian $T^n$-action (toric manifolds) are classified by their moment polytopes. $\mathbb{CP}^n$ corresponds to a simplex.
• Symplectic reduction (Meyer, 1973; Marsden–Weinstein, 1974): $\mu^{-1}(0)/T$ is again symplectic when the action on $\mu^{-1}(0)$ is free. For instance $\mathbb{CP}^{n-1}$ is the reduction of $\C^n$ by the diagonal circle action at a regular level of $\frac12 |z|^2$.
• Duistermaat–Heckman (1982): the push-forward of the Liouville measure by $\mu$ is piecewise polynomial — Archimedes' hat-box theorem is the case of $S^2$.

Contact geometry, the odd-dimensional sibling, studies hyperplane fields $\ker \alpha$ on a $(2n-1)$-manifold with $\alpha \wedge (d\alpha)^{n-1} \neq 0$ everywhere; energy hypersurfaces of Hamiltonian systems are often contact. The Weinstein conjecture (1979) asks whether every Reeb vector field on a closed contact manifold has a periodic orbit. Taubes proved it in dimension $3$ (2007), using Seiberg–Witten Floer theory; in higher dimensions it is known in many cases and open in general.

Mirror symmetry. Kontsevich's homological mirror symmetry conjecture (1994) predicts that the Fukaya category of a Calabi–Yau manifold $X$ — Lagrangian submanifolds, with morphisms given by Lagrangian Floer cohomology and compositions by counts of holomorphic polygons — is equivalent to the derived category of coherent sheaves on a mirror $X^\vee$ (see derived categories). It is proved in important cases: elliptic curves (Polishchuk–Zaslow, 1998), the quartic K3 surface (Seidel), and Calabi–Yau hypersurfaces in projective space (Sheridan, 2015). It is open in general.

A recent resolution. Viterbo conjectured (2000) that among convex domains in $\R^{2n}$ of a given volume the ball maximises every normalised capacity. In 2024 Haim-Kislev and Ostrover found a counterexample in $\R^4$, built from two pentagons. A single conjecture falling is a reminder that the subject is far from finished: questions as basic as "which symplectic manifolds of dimension $4$ exist, and which ellipsoids embed into which?" have rich, partly unexpected answers (McDuff and Schlenk found an infinite staircase governed by Fibonacci numbers for embedding ellipsoids into balls, 2012).

Mathlib has the symplectic group Matrix.symplecticGroup l R of matrices $A$ with $A J A^{\mathsf T} = J$, where $J$ is indexed by l ⊕ l, and two non-trivial facts about it. There are no symplectic manifolds in Mathlib yet, so Darboux's theorem, Moser's trick and Gromov's theorem are not formalised here. What is formalised is the linear algebra of the lesson and the conservation law, in full.

First, Theorem 4 (i), for any alternating form on any real normed space. Note that the proof never uses non-degeneracy:

/-- **Hamiltonian flows conserve the Hamiltonian.** Let `ω` be any alternating form on a real
normed space `V` (`ω v v = 0`), `H : V → ℝ` differentiable with derivative `dH z` at `z`, and `X`
the Hamiltonian vector field, defined by `ι_{X} ω = dH`, i.e. `ω (X z) w = dH z w`. Along any
flow line `γ' = X(γ)` the value `H(γ t)` is constant. Proof: by the chain rule
`(H ∘ γ)' = dH(γ)(X(γ)) = ω(X(γ), X(γ)) = 0`. Non-degeneracy of `ω` is what makes `X` exist and
be unique; it is not needed for conservation. -/
theorem hamiltonian_energy_conserved {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (ω : V → V → ℝ) (hω : ∀ v, ω v v = 0)
    {H : V → ℝ} {dH : V → V →L[ℝ] ℝ} (hH : ∀ z, HasFDerivAt H (dH z) z)
    {X : V → V} (hX : ∀ z w, ω (X z) w = dH z w)
    {γ : ℝ → V} (hγ : ∀ t, HasDerivAt γ (X (γ t)) t) (s t : ℝ) :
    H (γ s) = H (γ t) := by
  have hd : ∀ τ, HasDerivAt (fun τ => H (γ τ)) 0 τ := by
    intro τ
    have h := (hH (γ τ)).comp_hasDerivAt τ (hγ τ)
    have h0 : dH (γ τ) (X (γ τ)) = 0 := by rw [← hX, hω]
    rw [h0] at h
    exact h
  exact is_const_of_deriv_eq_zero (fun τ => (hd τ).differentiableAt) (fun τ => (hd τ).deriv) s t

In the plane, symplectic means determinant one (proved entry by entry), with the shear — the flow of a free particle — as the exercise:

/-- The standard symplectic matrix on ℝ² = {(q, p)}: `ω₀(u, v) = uᵀ J v = u₁ v₂ - u₂ v₁`, the
signed area of the parallelogram spanned by `u` and `v`. -/
def J2 : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1; -1, 0]

/-- For every real 2 × 2 matrix, `Aᵀ J A = (det A) J`: a linear map of the plane multiplies the
symplectic form, i.e. signed area, by its determinant. Proved entry by entry. -/
theorem transpose_mul_J2_mul (A : Matrix (Fin 2) (Fin 2) ℝ) :
    Aᵀ * J2 * A = A.det • J2 := by
  ext i j
  fin_cases i <;> fin_cases j <;>
    simp [J2, Matrix.mul_apply, Fin.sum_univ_two, Matrix.det_fin_two] <;> ring

/-- **In dimension two, symplectic means area- and orientation-preserving**: `Aᵀ J A = J` if
and only if `det A = 1`. In dimension four and higher this fails (see `squeeze`). -/
theorem symplectic_iff_det_eq_one (A : Matrix (Fin 2) (Fin 2) ℝ) :
    Aᵀ * J2 * A = J2 ↔ A.det = 1 := by
  rw [transpose_mul_J2_mul]
  constructor
  · intro h
    have := congrFun (congrFun h 0) 1
    simpa [J2] using this
  · intro h
    rw [h, one_smul]

/-- A shear `(q, p) ↦ (q + t p, p)` is symplectic: its determinant is `1`. (Solution of the Lean
exercise; it also describes the exact flow of the free particle `H = p²/2` for time `t`.) -/
theorem shear_symplectic (t : ℝ) :
    (!![1, t; 0, 1] : Matrix (Fin 2) (Fin 2) ℝ)ᵀ * J2 * !![1, t; 0, 1] = J2 := by
  rw [symplectic_iff_det_eq_one, Matrix.det_fin_two_of]
  ring

Evenness of dimension and the infinitesimal Liouville theorem:

/-- A skew-symmetric real matrix of odd size is singular: `det A = det Aᵀ = det (-A) =
(-1)ⁿ det A = -det A`. So an alternating bilinear form on an odd-dimensional space is always
degenerate, and a symplectic vector space (or manifold) has even dimension. -/
theorem det_eq_zero_of_skew_odd {n : ℕ} (hn : Odd n) (A : Matrix (Fin n) (Fin n) ℝ)
    (hA : Aᵀ = -A) : A.det = 0 := by
  have h1 : A.det = (-A).det := by rw [← hA, det_transpose]
  rw [det_neg, Fintype.card_fin, hn.neg_one_pow] at h1
  linarith

/-- **Linear Hamiltonian vector fields are divergence-free.** For a quadratic Hamiltonian
`H(z) = ½ zᵀ S z` the Hamiltonian vector field is linear, `X(z) = J S z` with `J` skew and `S`
symmetric, and its divergence is `trace (J S)`, which vanishes:
`tr(JS) = tr((JS)ᵀ) = tr(Sᵀ Jᵀ) = -tr(S J) = -tr(J S)`. This is Liouville's theorem at the level
of vector fields: the flow `exp(t J S)` has determinant `exp(t · tr(JS)) = 1`. -/
theorem trace_skew_mul_symm {n : ℕ} (J S : Matrix (Fin n) (Fin n) ℝ)
    (hJ : Jᵀ = -J) (hS : Sᵀ = S) : (J * S).trace = 0 := by
  have h : (J * S).trace = -(J * S).trace := by
    calc (J * S).trace = (J * S)ᵀ.trace := (trace_transpose _).symm
      _ = (Sᵀ * Jᵀ).trace := by rw [transpose_mul]
      _ = (S * -J).trace := by rw [hS, hJ]
      _ = -(S * J).trace := by rw [Matrix.mul_neg, trace_neg]
      _ = -(J * S).trace := by rw [trace_mul_comm]
  linarith

The linear Liouville theorem — symplectic matrices have determinant $1$ — is in Mathlib, with a surprisingly intricate proof (reduction to local rings). So is the fact that transposes of symplectic matrices are symplectic, used in Theorem 3:

/-- **Linear Liouville theorem**: every symplectic matrix (over any commutative ring) has
determinant `1`, so linear symplectic maps preserve volume. This applies Mathlib's
`SymplecticGroup.det_eq_one`, whose proof reduces to local rings and builds an invertible block
by hand; Mathlib's convention is `A * J * Aᵀ = J` with `J = !![0, -1; 1, 0]` in blocks. -/
theorem symplectic_det_eq_one {l : Type*} [DecidableEq l] [Fintype l]
    {A : Matrix (l ⊕ l) (l ⊕ l) ℝ} (hA : A ∈ symplecticGroup l ℝ) : A.det = 1 :=
  SymplecticGroup.det_eq_one hA

/-- The transpose of a symplectic matrix is symplectic (so `A * J * Aᵀ = J` and `Aᵀ * J * A = J`
define the same group). This applies Mathlib's `SymplecticGroup.transpose_mem`. It is why the
*rows* of a symplectic matrix pair up under `ω`, which the non-squeezing proof below uses. -/
theorem symplectic_transpose_mem {l : Type*} [DecidableEq l] [Fintype l]
    {A : Matrix (l ⊕ l) (l ⊕ l) ℝ} (hA : A ∈ symplecticGroup l ℝ) :
    Aᵀ ∈ symplecticGroup l ℝ :=
  SymplecticGroup.transpose_mem hA

Now Theorem 3 in $\R^4$, in coordinates $(x_1, y_1, x_2, y_2)$, with Mathlib's convention $A J A^{\mathsf T} = J$ so that the rows of $A$ pair under $\omega_0$ directly. The Wirtinger inequality is proved as a sum-of-squares identity in Plücker coordinates, and is slightly stronger than the Cauchy–Schwarz step the human proof needs:

/-- The standard symplectic matrix on ℝ⁴ with coordinates ordered `(x₁, y₁, x₂, y₂)`, so that
`ω₀ = dx₁ ∧ dy₁ + dx₂ ∧ dy₂`. -/
def J4 : Matrix (Fin 4) (Fin 4) ℝ :=
  !![0, 1, 0, 0; -1, 0, 0, 0; 0, 0, 0, 1; 0, 0, -1, 0]

/-- The standard symplectic form on ℝ⁴: the sum of the signed areas of the projections of the
parallelogram spanned by `u` and `v` to the `(x₁, y₁)`- and `(x₂, y₂)`-planes. -/
def omega4 (u v : Fin 4 → ℝ) : ℝ :=
  u 0 * v 1 - u 1 * v 0 + u 2 * v 3 - u 3 * v 2

/-- The entries of `A J Aᵀ` are the symplectic pairings of the rows of `A`:
`(A J Aᵀ)ᵢⱼ = ω₀(rowᵢ A, rowⱼ A)`. -/
theorem mul_J4_mul_transpose_apply (A : Matrix (Fin 4) (Fin 4) ℝ) (i j : Fin 4) :
    (A * J4 * Aᵀ) i j = omega4 (A i) (A j) := by
  simp [J4, omega4, Matrix.mul_apply, Fin.sum_univ_four]
  ring

/-- **A Wirtinger-type inequality in ℝ⁴**: `ω₀(a, b)² + ⟨a, b⟩² ≤ |a|² |b|²`. The symplectic area
of a parallelogram never exceeds its Euclidean area. Proof: the difference is the sum of squares
`(p₀₂ - p₁₃)² + (p₀₃ + p₁₂)²` of Plücker coordinates `pᵢⱼ = aᵢ bⱼ - aⱼ bᵢ` (an identity checked
by `ring`). -/
theorem wirtinger4 (a b : Fin 4 → ℝ) :
    omega4 a b ^ 2 + (a ⬝ᵥ b) ^ 2 ≤ (a ⬝ᵥ a) * (b ⬝ᵥ b) := by
  have key : (a ⬝ᵥ a) * (b ⬝ᵥ b) - (omega4 a b ^ 2 + (a ⬝ᵥ b) ^ 2) =
      ((a 0 * b 2 - a 2 * b 0) - (a 1 * b 3 - a 3 * b 1)) ^ 2 +
      ((a 0 * b 3 - a 3 * b 0) + (a 1 * b 2 - a 2 * b 1)) ^ 2 := by
    simp only [dotProduct, Fin.sum_univ_four, omega4]
    ring
  nlinarith [sq_nonneg ((a 0 * b 2 - a 2 * b 0) - (a 1 * b 3 - a 3 * b 1)),
    sq_nonneg ((a 0 * b 3 - a 3 * b 0) + (a 1 * b 2 - a 2 * b 1))]

/-- If `|a| ≥ 1`, the linear function `u ↦ ⟨a, u⟩` takes a value of size at least `r` on the
sphere of radius `r`: take `u = (r / |a|) a`, for which `⟨a, u⟩² = r² |a|² ≥ r²`. -/
theorem exists_long_shadow {a : Fin 4 → ℝ} (ha : 1 ≤ a ⬝ᵥ a) {r : ℝ} :
    ∃ u : Fin 4 → ℝ, u ⬝ᵥ u = r ^ 2 ∧ r ^ 2 ≤ (a ⬝ᵥ u) ^ 2 := by
  set s := Real.sqrt (a ⬝ᵥ a) with hs
  have hs2 : s ^ 2 = a ⬝ᵥ a := Real.sq_sqrt (by linarith)
  have hspos : 0 < s := Real.sqrt_pos.mpr (by linarith)
  refine ⟨(r / s) • a, ?_, ?_⟩
  · rw [smul_dotProduct, dotProduct_smul, smul_eq_mul, smul_eq_mul, ← hs2]
    field_simp
  · rw [dotProduct_smul, smul_eq_mul, mul_pow, div_pow, hs2]
    have h0 : 0 < a ⬝ᵥ a := by linarith
    rw [div_mul_eq_mul_div, le_div_iff₀ h0]
    nlinarith [mul_nonneg (sq_nonneg r) (mul_nonneg h0.le (sub_nonneg.mpr ha))]

/-- **Linear non-squeezing in ℝ⁴.** If a symplectic matrix `A` (here `A J Aᵀ = J`) maps the ball
`B⁴(r)` into the cylinder `Z(R) = {x₁² + y₁² ≤ R²}`, then `r ≤ R`. Proof: the first two rows
`a, b` of `A` satisfy `ω₀(a, b) = 1`, so by `wirtinger4` `|a|² |b|² ≥ 1` and one of them has
length at least `1`; `exists_long_shadow` then gives a point of `B⁴(r)` whose image lies at
distance at least `r` from the axis of the cylinder. Gromov's theorem says the same for all
symplectic *diffeomorphisms*; that needs pseudo-holomorphic curves and is not formalised. -/
theorem linear_nonsqueezing (A : Matrix (Fin 4) (Fin 4) ℝ) (hA : A * J4 * Aᵀ = J4)
    {r R : ℝ} (hR : 0 ≤ R)
    (hsub : ∀ u : Fin 4 → ℝ, u ⬝ᵥ u ≤ r ^ 2 → (A *ᵥ u) 0 ^ 2 + (A *ᵥ u) 1 ^ 2 ≤ R ^ 2) :
    r ≤ R := by
  -- the rows `a = A 0` and `b = A 1` satisfy `ω(a, b) = 1`
  have hab : omega4 (A 0) (A 1) = 1 := by
    rw [← mul_J4_mul_transpose_apply, hA]; simp [J4]
  have hw := wirtinger4 (A 0) (A 1)
  rw [hab] at hw
  have ha0 := dot_self_nonneg (A 0)
  have hb0 := dot_self_nonneg (A 1)
  -- one of the two rows has length at least one
  have hlong : 1 ≤ A 0 ⬝ᵥ A 0 ∨ 1 ≤ A 1 ⬝ᵥ A 1 := by
    rcases le_or_gt 1 (A 0 ⬝ᵥ A 0) with h | h
    · exact Or.inl h
    · rcases le_or_gt 1 (A 1 ⬝ᵥ A 1) with h' | h'
      · exact Or.inr h'
      · nlinarith [sq_nonneg (A 0 ⬝ᵥ A 1), mul_le_mul h.le h'.le hb0 zero_le_one]
  -- so some point of the ball lands at distance ≥ r from the axis
  have hr2 : r ^ 2 ≤ R ^ 2 := by
    rcases hlong with h | h
    · obtain ⟨u, hu, hshadow⟩ := exists_long_shadow h (r := r)
      have := hsub u hu.le
      simp only [mulVec] at this
      nlinarith [sq_nonneg (A 1 ⬝ᵥ u)]
    · obtain ⟨u, hu, hshadow⟩ := exists_long_shadow h (r := r)
      have := hsub u hu.le
      simp only [mulVec] at this
      nlinarith [sq_nonneg (A 0 ⬝ᵥ u)]
  nlinarith

Finally the contrast: a volume-preserving matrix that is not symplectic and does squeeze the unit ball into the cylinder of radius $\frac12$ — impossible for a symplectic matrix by the previous theorem.

/-- The squeeze `(x₁, y₁, x₂, y₂) ↦ (x₁/2, y₁/2, 2x₂, 2y₂)`: it shrinks the first symplectic
plane and stretches the second. -/
noncomputable def squeeze : Matrix (Fin 4) (Fin 4) ℝ := Matrix.diagonal ![1 / 2, 1 / 2, 2, 2]

/-- The squeeze preserves volume: `det = ½ · ½ · 2 · 2 = 1`. -/
theorem squeeze_det : squeeze.det = 1 := by
  simp [squeeze, Matrix.det_diagonal, Fin.prod_univ_four]

/-- The squeeze is not symplectic: it multiplies `ω₀(e₁, e₂) = 1` by `¼`. -/
theorem squeeze_not_symplectic : squeeze * J4 * squeezeᵀ ≠ J4 := by
  intro h
  have := congrFun (congrFun h 0) 1
  simp [squeeze, J4, Matrix.mul_apply, Fin.sum_univ_four] at this
  norm_num at this

/-- The squeeze maps the unit ball `B⁴(1)` into the thin cylinder `Z(1/2)`. Together with
`linear_nonsqueezing` this shows that volume preservation is far weaker than being symplectic:
no symplectic matrix can do this. -/
theorem squeeze_ball (u : Fin 4 → ℝ) (hu : u ⬝ᵥ u ≤ 1) :
    (squeeze *ᵥ u) 0 ^ 2 + (squeeze *ᵥ u) 1 ^ 2 ≤ (1 / 2) ^ 2 := by
  simp only [squeeze, mulVec_diagonal]
  simp only [dotProduct, Fin.sum_univ_four] at hu
  simp
  nlinarith [sq_nonneg (u 2), sq_nonneg (u 3)]

Not formalised: symplectic manifolds and Hamiltonian vector fields on them; Theorem 1 as a basis statement (only evenness is proved); Theorem 3 in dimensions other than four; Moser's trick and Darboux's theorem; pseudo-holomorphic curves, Gromov's theorem, the Arnold conjecture and Floer homology. Formalising Floer theory is far beyond any current proof assistant library.

Numerical analysts met symplectic geometry from the other side. A one-step method for Hamilton's equations is symplectic if each step is a symplectic map. Symplectic methods do not conserve energy exactly, but backward error analysis shows that (for analytic Hamiltonians and small steps) a symplectic method agrees, up to exponentially small errors, with the exact flow of a nearby modified Hamiltonian, so the energy error stays bounded over exponentially long times instead of drifting. The first experiment integrates the pendulum with two non-symplectic methods (explicit Euler, RK4) and two symplectic ones (symplectic Euler, leapfrog), and computes exactly how one step of each changes phase-space area for the harmonic oscillator.

"""Symplectic and non-symplectic integrators for the pendulum.

Hamilton's equations for the pendulum H(q, p) = p^2/2 - cos q are solved
numerically by four one-step methods. Explicit Euler and the classical
Runge-Kutta method (RK4) are not symplectic; symplectic Euler and the
Stormer-Verlet (leapfrog) method are. We record the energy error over a long
run, and for the harmonic oscillator H = (q^2 + p^2)/2 we compute, with exact
fractions, the determinant of one step of each method: the factor by which
the step multiplies phase-space area.

Evidence: numerical (floating-point runs of finitely many steps) and exact
(rational determinants for one step size). Neither replaces the theorems
(Liouville's theorem; backward error analysis for symplectic methods).
"""

import math
from fractions import Fraction

def energy(q, p):
    """The pendulum Hamiltonian H(q, p) = p^2/2 - cos q."""
    return p * p / 2 - math.cos(q)

def force(q):
    """-dH/dq for the pendulum."""
    return -math.sin(q)

def explicit_euler(q, p, h):
    """One explicit Euler step (not symplectic)."""
    return q + h * p, p + h * force(q)

def symplectic_euler(q, p, h):
    """Kick then drift: p <- p + h F(q), q <- q + h p (symplectic)."""
    p = p + h * force(q)
    return q + h * p, p

def leapfrog(q, p, h):
    """Stormer-Verlet: half kick, drift, half kick (symplectic, order 2)."""
    p = p + h / 2 * force(q)
    q = q + h * p
    return q, p + h / 2 * force(q)

def rk4(q, p, h):
    """Classical fourth-order Runge-Kutta step (not symplectic)."""
    def f(a, b):
        return b, force(a)
    k1 = f(q, p)
    k2 = f(q + h / 2 * k1[0], p + h / 2 * k1[1])
    k3 = f(q + h / 2 * k2[0], p + h / 2 * k2[1])
    k4 = f(q + h * k3[0], p + h * k3[1])
    q = q + h / 6 * (k1[0] + 2 * k2[0] + 2 * k3[0] + k4[0])
    p = p + h / 6 * (k1[1] + 2 * k2[1] + 2 * k3[1] + k4[1])
    return q, p

METHODS = [
    ("explicit Euler", explicit_euler),
    ("symplectic Euler", symplectic_euler),
    ("leapfrog", leapfrog),
    ("RK4", rk4),
]

def energy_errors(step, q, p, h, n, checkpoints):
    """Run n steps; return {k: max |H - H0| over the first k steps}."""
    e0 = energy(q, p)
    out, worst = {}, 0.0
    for k in range(1, n + 1):
        q, p = step(q, p, h)
        worst = max(worst, abs(energy(q, p) - e0))
        if k in checkpoints:
            out[k] = worst
    return out

def oscillator_step_matrix(name, h):
    """Exact 2x2 matrix of one step for H = (q^2 + p^2)/2, entries Fractions."""
    h = Fraction(h)
    if name == "explicit Euler":
        return [[1, h], [-h, 1]]
    if name == "symplectic Euler":
        return [[1 - h * h, h], [-h, 1]]
    if name == "leapfrog":
        return [[1 - h * h / 2, h], [-h + h ** 3 / 4, 1 - h * h / 2]]
    if name == "RK4":
        a = 1 - h ** 2 / 2 + h ** 4 / 24
        b = h - h ** 3 / 6
        return [[a, b], [-b, a]]
    raise ValueError(name)

def det2(m):
    """Determinant of a 2x2 matrix."""
    return m[0][0] * m[1][1] - m[0][1] * m[1][0]

def main():
    h, n, checks = 0.2, 40000, (100, 1000, 10000, 40000)
    print("Pendulum H = p^2/2 - cos q, start (q, p) = (2, 0), step h = 0.2")
    print("Largest energy error max|H - H0| up to time t:")
    print(f"{'method':<18}" + "".join(f"{f't = {k * h:g}':>15}"
                                      for k in checks))
    for name, step in METHODS:
        errs = energy_errors(step, 2.0, 0.0, h, n, set(checks))
        print(f"{name:<18}" + "".join(f"{errs[k]:>15.2e}" for k in checks))
    print()
    print("One step for H = (q^2 + p^2)/2 with h = 1/10: exact det of the map")
    for name, _ in METHODS:
        d = det2(oscillator_step_matrix(name, Fraction(1, 10)))
        print(f"  {name:<18} det = {str(d):<26} ~ {float(d):.12f}")
    grow = float(Fraction(101, 100) ** 1000)
    print(f"Explicit Euler multiplies area by (1.01)^1000 ~ {grow:.3g} "
          "in 1000 steps.")
    print()
    print("Epistemic status: the energy table is numerical evidence from")
    print("floating-point runs of finitely many steps; it shows bounded energy")
    print("error for the two symplectic methods and growth (fast for explicit")
    print("Euler, slow for RK4) for the others, but proves nothing about all")
    print("times. The determinants are exact: the symplectic steps preserve")
    print("area exactly, while Euler expands it and RK4 contracts it slightly.")

if __name__ == "__main__":
    main()