The standard symplectic form is compatible with $\tilde J$

Proved

FiniteEnergyPlane.omega0_tames_jtilde

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

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)$ be a strictly star-shaped level and $J$ a smooth $d\lambda_0$ -compatible complex structure on $\xi$ . For every $y\neq0$ : $\omega_0(v,\tilde J(y)v)>0$ for all $v\neq0$ , and $\omega_0(\tilde J(y)v,\tilde J(y)w)=\omega_0(v,w)$ for all $v,w$ .

Formalization Note $\omega_0$ is the constant form omega0 on $V$ (not a form on $\mathbb{R}\times S$ ).

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- The standard symplectic form and the symplectization structure. At every `y ≠ 0`, `ω₀` is
compatible with `J̃(y)`: `ω₀(v, J̃ v) > 0` for `v ≠ 0`, and `ω₀(J̃ v, J̃ w) = ω₀(v, w)`. -/
theorem omega0_tames_jtilde {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (y : V n) (hy : y ≠ 0) :
    (∀ v : V n, v ≠ 0 → 0 < omega0 v (Jtilde H J y v)) ∧
      ∀ v w : V n, omega0 (Jtilde H J y v) (Jtilde H J y w) = omega0 v w := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Section 2.2

Read-back

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

Read-back: `FiniteEnergyPlane.omega0_tames_jtilde`

Setting. Fix a natural number $n \ge 0$ (implicit) and let $V = \mathbb{R}^{2(n+1)}$ , with coordinates indexed $0, 1, \dots, 2n+1$ (so $\dim V \ge 2$ ). The following fixed structures are used:

$j_0 : V \to V$ is the linear map with $(j_0 v)_k = -v_{k+1}$ for $k$ even and $(j_0 v)_k = v_{k-1}$ for $k$ odd; on each coordinate pair $(v_{2i}, v_{2i+1})$ it acts as $(a, b) \mapsto (-b, a)$ .
$\omega_0(u, v) = \sum_k (j_0 u)_k\, v_k = \sum_i \big(u_{2i} v_{2i+1} - u_{2i+1} v_{2i}\big)$ .
$\lambda_x(v) = \tfrac12 \omega_0(x, v)$ for $x, v \in V$ .
For $H : V \to \mathbb{R}$ , $dH_x$ is the Fréchet derivative of $H$ at $x$ (by convention the zero map where $H$ is not differentiable); $\nabla H(x)$ has components $dH_x(e_k)$ ; $X_H(x) = j_0 \nabla H(x)$ ; $R(x) = \lambda_x(X_H(x))^{-1} X_H(x)$ (with $0^{-1} = 0$ ).
$\xi_x = \{ v \in V : \lambda_x(v) = 0 \text{ and } dH_x(v) = 0 \}$ , and $S = \{x : H(x) = 1\}$ .

Hypotheses.

$H : V \to \mathbb{R}$ such that (i) $H$ is $C^\infty$ ; (ii) for every $u \ne 0$ there is exactly one $r \in \mathbb{R}$ with $r > 0$ and $H(r u) = 1$ ; (iii) for every $x$ with $H(x) = 1$ , $dH_x(x) > 0$ .
$J : V \to \mathcal{L}(V, V)$ (continuous linear endomorphisms of $V$ ) such that $J$ is $C^\infty$ , and for every $x \in S$ and all $v, w \in \xi_x$ : $J(x) v \in \xi_x$ ; $J(x)J(x) v = -v$ ; if $v \ne 0$ then $\omega_0(v, J(x) v) > 0$ ; and $\omega_0(J(x) v, J(x) w) = \omega_0(v, w)$ . No condition is placed on $J(x)$ outside $\xi_x$ , nor on $J(x)$ for $x \notin S$ , beyond global smoothness.
A point $y \in V$ with $y \ne 0$ .

Auxiliary maps. $s(y)$ is a (choice-function-selected) $r > 0$ with $H(r y) = 1$ if such an $r$ exists, and $s(y) = 1$ otherwise; for $y \ne 0$ it is the unique such $r$ by (ii). Put $x = \pi(y) = s(y)\, y$ and $r = s(y)$ , and define, for $v \in V$ ,

\alpha(v) = \frac{r}{2\, dH_x(x)}\, dH_x(v) \ \ (\text{the fraction is } 0 \text{ if } dH_x(x) = 0), \qquad \beta(v) = r\, \lambda_x(v),

w(v) = v - \alpha(v)\,(2y) - \beta(v)\, r^{-1} R(x),

\tilde J(y)\, v = \alpha(v)\, r^{-1} R(x) - \beta(v)\,(2y) + J(x)\big(w(v)\big).

Conclusion. Both of the following hold for this $y$ :

for every $v \in V$ with $v \ne 0$ : $\omega_0\big(v, \tilde J(y) v\big) > 0$ ;
for all $v, w \in V$ : $\omega_0\big(\tilde J(y) v, \tilde J(y) w\big) = \omega_0(v, w)$ .

Both statements are over all of $V$ (not only over $\xi_x$ ).

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

The standard symplectic form is compatible with J~\tilde JJ~

Read-back: FiniteEnergyPlane.omega0_tames_jtilde

The standard symplectic form is compatible with $\tilde J$

Read-back: `FiniteEnergyPlane.omega0_tames_jtilde`