The asymptotic operator in a unitary frame

Proved

FiniteEnergyPlane.asympOp_frame_bridge

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

asymptotic-operatorpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)$ be a strictly star-shaped level, $J$ a smooth $d\lambda_0$ -compatible complex structure on $\xi$ , and $P=(x,T)$ a periodic Reeb orbit. A unitary frame $Z$ of $\xi$ along $P$ exists. For every unitary frame $Z$ there is a $C^\infty$ $1$ -periodic loop $S_\infty$ of symmetric $2n\times2n$ matrices such that

A_P\big(Z\eta\big)(t)=Z(t)\big(-J_0\eta'(t)-S_\infty(t)\eta(t)\big)

for every $C^\infty$ $1$ -periodic $\eta:\mathbb{R}\to\mathbb{R}^{2n}$ and every $t$ , and $P$ is nondegenerate if and only if the asymptotic operator $-J_0\partial_t-S_\infty$ is nondegenerate.

Formalization Note $Z\eta$ is fun t => Z t (η t). Symmetric loops and nondegeneracy are CauchyRiemannIndex.IsSymLoop and CauchyRiemannIndex.IsNondegenerate (no fundamental solution of $\Psi'=J_0S_\infty\Psi$ , $\Psi(0)=1$ , has $\det(1-\Psi(1))=0$ ).

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hryniewicz, Remark 2.6: a unitary frame of `ξ` along `P` exists, and in any such frame `Z`
the asymptotic operator takes the form `-J₀ ∂ₜ - S∞(t)` for a smooth loop `S∞` of symmetric
matrices: `A_P (Z η) = Z (-J₀ η' - S∞ η)`. Moreover `P` is nondegenerate if and only if
`-J₀ ∂ₜ - S∞` is nondegenerate in the sense of `CauchyRiemannIndex.IsNondegenerate`. -/
theorem asympOp_frame_bridge {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (P : ReebOrbit H) :
    (∃ Z : ℝ → CauchyRiemannIndex.Vec n →L[ℝ] V n, IsUnitaryXiFrame J P Z) ∧
      ∀ Z : ℝ → CauchyRiemannIndex.Vec n →L[ℝ] V n, IsUnitaryXiFrame J P Z →
        ∃ Sinf : ℝ → CauchyRiemannIndex.Mat n, CauchyRiemannIndex.IsSymLoop Sinf ∧
          (∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j)) ∧
          (∀ η : ℝ → CauchyRiemannIndex.Vec n, ContDiff ℝ ∞ η → Function.Periodic η 1 →
            ∀ t : ℝ, asympOp J P (fun t => Z t (η t)) t =
              Z t (-(Matrix.toEuclideanLin (CauchyRiemannIndex.J₀ n) (deriv η t)) -
                Matrix.toEuclideanLin (Sinf t) (η t))) ∧
          (P.IsNondegenerate ↔ CauchyRiemannIndex.IsNondegenerate Sinf) := 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, Remark 2.6

Read-back

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

Read-back: `FiniteEnergyPlane.asympOp_frame_bridge`

Setting. Fix $n \in \mathbb N$ (including $n = 0$ ).

$V = \mathbb R^{2n+2}$ with coordinates $v_0, \dots, v_{2n+1}$ . Write $(j_0 v)_{2i} = -v_{2i+1}$ , $(j_0 v)_{2i+1} = v_{2i}$ , $\langle u, v\rangle = \sum_k u_k v_k$ , $\omega_0(u, v) = \langle j_0 u, v\rangle = \sum_i (u_{2i} v_{2i+1} - u_{2i+1} v_{2i})$ and $\lambda_x(v) = \tfrac12\, \omega_0(x, v)$ .
For $H : V \to \mathbb R$ , $dH_x$ is the Fréchet derivative at $x$ (the zero map where $H$ is not differentiable), $\nabla H(x) = (dH_x(e_k))_k$ , $X_H = j_0 \nabla H$ , and the Reeb field is $R(x) = \lambda_x(X_H(x))^{-1} X_H(x)$ with $0^{-1} = 0$ ; $DR(x)$ is its Fréchet derivative (zero where $R$ is not differentiable). $\xi_x = \{v : \lambda_x(v) = 0,\ dH_x(v) = 0\}$ .
$E = \mathbb R^{2n}$ with coordinates $(a_1,\dots,a_n,b_1,\dots,b_n)$ and the Euclidean inner product $\langle\cdot,\cdot\rangle_E$ . $\mathrm{Mat}$ denotes real $2n \times 2n$ matrices indexed the same way, acting on $E$ by matrix multiplication. $J_0 = \begin{pmatrix} 0 & -I \\ I & 0\end{pmatrix}$ , so $J_0(a,b) = (-b,a)$ .

Hypotheses.

$H$ is strictly star-shaped: $H$ is $C^\infty$ ; for every $u \neq 0$ there is exactly one $r > 0$ with $H(r u) = 1$ ; and $dH_x(x) > 0$ whenever $H(x) = 1$ .
$J$ assigns to each $x \in V$ a linear map $J_x : V \to V$ and is compatible with $\xi$ : $x \mapsto J_x$ is $C^\infty$ , and for every $x$ with $H(x) = 1$ and all $v, w \in \xi_x$ : $J_x v \in \xi_x$ , $J_x J_x v = -v$ , $\omega_0(v, J_x v) > 0$ if $v \neq 0$ , and $\omega_0(J_x v, J_x w) = \omega_0(v, w)$ .
$P$ is a Reeb orbit of $H$ : $x_P : \mathbb R \to V$ and $T_P > 0$ with $H(x_P(\tau)) = 1$ , $x_P'(\tau) = R(x_P(\tau))$ and $x_P(\tau + T_P) = x_P(\tau)$ for all $\tau$ .

Terms used in the conclusion.

A unitary $\xi$ -frame along $P$ is $Z : \mathbb R \to \mathrm L(E, V)$ which is $C^\infty$ and $1$ -periodic and such that, for every $t$ with $x = x_P(T_P t)$ : $Z(t)a \in \xi_x$ for all $a \in E$ ; every $w \in \xi_x$ equals $Z(t)a$ for some $a$ ; $J_x Z(t) a = Z(t) J_0 a$ for all $a$ ; and $\omega_0(Z(t)a, Z(t)b) = \langle J_0 a, b\rangle_E$ for all $a, b$ .
The asymptotic operator on $\gamma : \mathbb R \to V$ : $(A\gamma)(t) = J_{x_P(T_P t)}\bigl( -\gamma'(t) + T_P\, DR(x_P(T_P t))\, \gamma(t) \bigr)$ .
$P$ is nondegenerate if for every $\Phi : \mathbb R \to \mathrm L(V,V)$ with $\Phi(0) = \mathrm{id}$ and $\Phi'(\tau) = DR(x_P(\tau)) \circ \Phi(\tau)$ for all $\tau$ , and every $v \in \xi_{x_P(0)}$ , $\Phi(T_P)v = v$ implies $v = 0$ .
$S_\infty : \mathbb R \to \mathrm{Mat}$ is a symmetric loop if it is continuous, $1$ -periodic and each $S_\infty(t)$ is a symmetric matrix.
$S_\infty$ is nondegenerate in the matrix sense if every $\Psi : \mathbb R \to \mathrm{Mat}$ with $\Psi(0) = I$ and $\Psi'(t) = J_0 S_\infty(t) \Psi(t)$ for all $t$ satisfies $\det(I - \Psi(1)) \neq 0$ .

Conclusion. Both of the following hold.

A unitary $\xi$ -frame $Z$ along $P$ exists.
For every unitary $\xi$ $ξ$ -frame $Z$ $Z$ along $P$ $P$ there is $S_\infty : \mathbb R \to \mathrm{Mat}$ $S_{\infty} : R \to Mat$ (depending on $Z$ $Z$ ) such that:
- $S_\infty$ is a symmetric loop, and every entry $t \mapsto S_\infty(t)_{ij}$ is $C^\infty$ ;
- for every $C^\infty$ , $1$ -periodic $\eta : \mathbb R \to E$ and every $t \in \mathbb R$ ,

A\bigl( s \mapsto Z(s)\,\eta(s) \bigr)(t) = Z(t)\Bigl( -J_0\, \eta'(t) - S_\infty(t)\, \eta(t) \Bigr);

$P$ is nondegenerate if and only if $S_\infty$ is nondegenerate in the matrix sense.

For $n = 0$ , $E$ is the zero space, so a unitary $\xi$ -frame forces $\xi_{x_P(T_P t)} = \{0\}$ for every $t$ , and part 1 then asserts that these spaces are all zero.

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 asymptotic operator in a unitary frame

Read-back: FiniteEnergyPlane.asympOp_frame_bridge

Read-back: `FiniteEnergyPlane.asympOp_frame_bridge`