Ellipsoids: both axes bind adapted open books with disk-like pages

Proved

HryniewiczCriterion.ellipsoid_axes_bind_adapted_open_books

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

contact-geometrydynamical-systemssymplectic-geometry

Let $r_1,r_2>0$ and let $S$ be the boundary of the ellipsoid

\frac{q_1^2+p_1^2}{r_1^2}+\frac{q_2^2+p_2^2}{r_2^2}=1.

Let $P$ be a prime periodic orbit of $X_H$ on $S$ , with $H$ the left-hand side, whose image lies in one of the two axes $\{q_2=p_2=0\}$ or $\{q_1=p_1=0\}$ . Then $P$ is the binding of an open book decomposition of $S$ with disk-like pages that is adapted to the flow: every page is a disk-like global surface of section with oriented boundary $P$ .

Hryniewicz notes that the axes of an ellipsoid are bindings of adapted open books, while the Hofer–Wysocki–Zehnder theorem detects only the axis of smaller action. The statement is an explicit example of the notions used in Theorems 1.7 and 1.8. It checks that the definitions of global sections and open books are satisfiable.

Preamble

import Definitions.Def_HryniewiczCriterion_GlobalSection

Formal statement

namespace HryniewiczCriterion

/-- Hryniewicz, p. 3: on the boundary of an ellipsoid, each of the two axis circles is
the binding of an adapted open book decomposition with disk-like pages. -/
theorem ellipsoid_axes_bind_adapted_open_books (r₁ r₂ : ℝ) (h₁ : 0 < r₁) (h₂ : 0 < r₂)
    (P : PeriodicOrbit
      (fun x : R4 => (x 0 ^ 2 + x 1 ^ 2) / r₁ ^ 2 + (x 2 ^ 2 + x 3 ^ 2) / r₂ ^ 2))
    (hP : P.IsPrime)
    (haxis : P.image ⊆ {x | x 2 = 0 ∧ x 3 = 0} ∨ P.image ⊆ {x | x 0 = 0 ∧ x 1 = 0}) :
    HasAdaptedDiskOpenBook
      (fun x : R4 => (x 0 ^ 2 + x 1 ^ 2) / r₁ ^ 2 + (x 2 ^ 2 + x 3 ^ 2) / r₂ ^ 2) P := by sorry

end HryniewiczCriterion

Source

Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014) 791-862, https://arxiv.org/abs/1105.2077, p. 3, paragraph after Theorem 1.7

Read-back

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

Read-back. Let $r_1, r_2$ be real numbers with $r_1 > 0$ and $r_2 > 0$ (equality $r_1 = r_2$ is allowed). Coordinates on $\mathbb{R}^4$ are $x = (x_0,x_1,x_2,x_3)$ and the Hamiltonian is the fixed quadratic

H(x) = \frac{x_0^2 + x_1^2}{r_1^2} + \frac{x_2^2 + x_3^2}{r_2^2}, \qquad \Sigma = \{x : H(x) = 1\}.

The Hamiltonian vector field is $X_H(x) = (-\partial_1 H, \partial_0 H, -\partial_3 H, \partial_2 H)(x)$ , here $X_H(x) = \bigl(-2x_1/r_1^2,\ 2x_0/r_1^2,\ -2x_3/r_2^2,\ 2x_2/r_2^2\bigr)$ . A trajectory is a curve $y:\mathbb{R}\to\mathbb{R}^4$ with $y'(t) = X_H(y(t))$ and $H(y(t)) = 1$ for all $t \in \mathbb{R}$ .

Hypotheses on the orbit.

$P$ is a periodic orbit: a trajectory $x : \mathbb{R} \to \mathbb{R}^4$ together with a real $T > 0$ such that $x(t + T) = x(t)$ for all $t$ .
(prime) $x(t) \neq x(0)$ for every $0 < t < T$ .
(axis) the image $x(\mathbb{R})$ lies in the plane $\{x_2 = x_3 = 0\}$ , or it lies in the plane $\{x_0 = x_1 = 0\}$ .

Conclusion. There exists a family $p : \mathbb{R} \times \mathbb{R}^2 \to \mathbb{R}^4$ , written $p_\theta(u)$ , with all of the following properties. Here $D = \{u_0^2+u_1^2 \le 1\}$ is the closed unit disk, $\mathring D = \{u_0^2+u_1^2 < 1\}$ the open disk, $S^1 = \{u_0^2+u_1^2 = 1\}$ the unit circle, and $\omega_0(a,b) = a_0b_1 - a_1b_0 + a_2b_3 - a_3b_2$ .

Smooth: $(\theta, u) \mapsto p_\theta(u)$ is $C^\infty$ on all of $\mathbb{R} \times \mathbb{R}^2$ .
Periodic in $\theta$ : $p_{\theta+1}(u) = p_\theta(u)$ for all $\theta, u$ .
Each page is a disk-like global section for $P$ : for every $\theta$ $θ$ , the map $e = p_\theta$ $e = p_{θ}$ satisfies
- $e$ is $C^\infty$ on $\mathbb{R}^2$ , injective on $D$ , and its derivative $De(u)$ is injective for every $u \in D$ ;
- $e(D) \subseteq \Sigma$ ;
- $e(S^1) = x(\mathbb{R})$ (equality of sets);
- for every $u \in \mathring D$ , $X_H(e(u))$ is not in the image of $De(u)$ ;
- for every trajectory $y$ with $y(0) \notin x(\mathbb{R})$ and every $a \in \mathbb{R}$ , there exist $t > a$ with $y(t) \in e(D)$ and $t' < a$ with $y(t') \in e(D)$ (the trajectory meets the image of the closed disk at arbitrarily late and arbitrarily early times).
Common binding, parametrized by the orbit: for all $\theta, t \in \mathbb{R}$ ,

p_\theta(\cos 2\pi t,\ \sin 2\pi t) = x(Tt).

Positivity: for all $\theta$ and $u \in \mathring D$ ,

\omega_0\bigl(\partial_{u_0} p_\theta(u),\ \partial_{u_1} p_\theta(u)\bigr) > 0.

Fibration: for every $y \in \Sigma$ with $y \notin x(\mathbb{R})$ there is exactly one pair $(\theta, u)$ with $\theta \in [0,1)$ , $u \in \mathring D$ and $p_\theta(u) = y$ .
Regularity: for every $\theta \in \mathbb{R}$ and $u \in \mathring D$ , the derivative of $(\theta,u)\mapsto p_\theta(u)$ at $(\theta,u)$ , a linear map $\mathbb{R}\times\mathbb{R}^2 \to \mathbb{R}^4$ , is injective.

Edge cases. The theorem is stated for the given parametrization $x$ of $P$ (including its starting point $x(0)$ and period $T$ ); property 4 ties all pages to that parametrization. The primality hypothesis makes $T$ the minimal positive time of return to $x(0)$ . The axis hypothesis is a disjunction; nothing further about which plane is required. No statement is made about pages for $\theta$ beyond what periodicity and properties 3–7 give.

Human review

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

View graph