Disk-like global surfaces of section, unknots, adapted open books

Definition

HryniewiczCriterion_GlobalSection

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

contact-geometrydynamical-systemssymplectic-geometry

Let $S=H^{-1}(1)\subset\mathbb{R}^4$ carry the flow of $X_H$ , and let $P=(x,T)$ be a periodic orbit. Write $\mathbb{D}$ for the closed unit disk in $\mathbb{R}^2$ and $\partial\mathbb{D}$ for the unit circle.

A smooth disk embedding is a smooth map $e:\mathbb{R}^2\to\mathbb{R}^4$ that is injective on $\mathbb{D}$ and has injective differential at every point of $\mathbb{D}$ , boundary included.
$P$ $P$ bounds a disk-like global surface of section if there is a smooth disk embedding $e$ $e$ with $D=e(\mathbb{D})\subset S$ $D = e (D) \subset S$ such that
1. $e(\partial\mathbb{D})=x(\mathbb{R})$ ;
2. $X_H$ is transverse to $D\setminus\partial D$ , i.e. $X_H(e(u))\notin \operatorname{im} de(u)$ for $|u|<1$ ;
3. every trajectory $y$ on $S$ with $y(0)\notin x(\mathbb{R})$ meets $D$ at arbitrarily large positive and arbitrarily large negative times.
$P$ is unknotted if $x(\mathbb{R})=e(\partial\mathbb{D})$ for some smooth disk embedding $e$ with $e(\mathbb{D})\subset S$ .
An adapted open book decomposition with disk-like pages and binding $P$ is a smooth family $\theta\mapsto e_\theta$ $θ \mapsto e_{θ}$ , $\theta\in\mathbb{R}/\mathbb{Z}$ $θ \in R / Z$ , such that:
1. every $e_\theta$ parametrizes a disk-like global surface of section bounded by $P$ ;
2. $e_\theta(\cos2\pi t,\sin2\pi t)=x(Tt)$ for all $\theta,t$ , so the binding carries the orientation of the flow;
3. every page is positively oriented by $d\lambda_0=\omega_0$ ;
4. $(\theta,u)\mapsto e_\theta(u)$ maps $\mathbb{R}/\mathbb{Z}\times\operatorname{int}\mathbb{D}$ bijectively onto $S\setminus x(\mathbb{R})$ with injective differential. Then $\theta$ is a smooth fibration $S\setminus x(\mathbb{R})\to\mathbb{R}/\mathbb{Z}$ whose fibres are the interiors of the pages, as in Definition 1.2.

These are the notions in which Hryniewicz's criterion (Theorem 1.7) and Theorem 1.8 are stated.

Formalization Note Smoothness up to the boundary of $\mathbb{D}$ is encoded by asking for a smooth map on all of $\mathbb{R}^2$ . The open book stores a page map ℝ → ℝ² → ℝ⁴, $1$ -periodic in $\theta$ , together with its properties.

Definition code

import Definitions.Def_HryniewiczCriterion_Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

/-!
# Disk-like global surfaces of section, unknots and adapted open books

Hryniewicz, arXiv:1105.2077, §1 (pp. 1–2): global surfaces of section, open book
decompositions and Definition 1.2 (adapted open books), specialized to disk-like
surfaces on a star-shaped level `S = H⁻¹(1)` with the flow of `X_H`.
-/

namespace HryniewiczCriterion

noncomputable section

open scoped ContDiff

/-- Parameter plane `ℝ²` of a disk. -/
abbrev Plane := Fin 2 → ℝ

def closedUnitDisk : Set Plane := {u | u 0 ^ 2 + u 1 ^ 2 ≤ 1}

def openUnitDisk : Set Plane := {u | u 0 ^ 2 + u 1 ^ 2 < 1}

def unitCircle : Set Plane := {u | u 0 ^ 2 + u 1 ^ 2 = 1}

/-- The point `(cos 2πt, sin 2πt)`; it runs once counterclockwise around the unit
circle as `t` runs over `[0, 1]`. -/
def circlePoint (t : ℝ) : Plane := ![Real.cos (2 * Real.pi * t), Real.sin (2 * Real.pi * t)]

/-- `e` restricts to a smooth embedding of the closed unit disk: `e` is smooth,
injective on the disk, with injective differential at every point of the disk
(boundary included). -/
def IsSmoothDiskEmbedding (e : Plane → R4) : Prop :=
  ContDiff ℝ ∞ e ∧ Set.InjOn e closedUnitDisk ∧
    ∀ u ∈ closedUnitDisk, Function.Injective (fderiv ℝ e u)

/-- `e` parametrizes a disk-like global surface of section `D = e(closed disk) ⊆ S`
bounded by `P`: `∂D = e(circle)` is the image of `P`; `X_H` is transverse to
`D \ ∂D`; and every trajectory on `S` not contained in `∂D` meets `D` at arbitrarily
large positive and at arbitrarily large negative times. -/
def IsDiskLikeGlobalSectionMap (H : R4 → ℝ) (P : PeriodicOrbit H) (e : Plane → R4) :
    Prop :=
  IsSmoothDiskEmbedding e ∧
  e '' closedUnitDisk ⊆ energySurface H ∧
  e '' unitCircle = P.image ∧
  (∀ u ∈ openUnitDisk,
    hamiltonianVectorField H (e u) ∉ Set.range (fderiv ℝ e u)) ∧
  ∀ y : ℝ → R4, IsTrajectory H y → y 0 ∉ P.image → ∀ a : ℝ,
    (∃ t, a < t ∧ y t ∈ e '' closedUnitDisk) ∧ (∃ t, t < a ∧ y t ∈ e '' closedUnitDisk)

/-- `P` bounds a disk-like global surface of section. -/
def BoundsDiskLikeGlobalSection (H : R4 → ℝ) (P : PeriodicOrbit H) : Prop :=
  ∃ e : Plane → R4, IsDiskLikeGlobalSectionMap H P e

/-- `P` is unknotted: its image is the boundary of a smoothly embedded closed disk
in `S`. -/
def IsUnknotted (H : R4 → ℝ) (P : PeriodicOrbit H) : Prop :=
  ∃ e : Plane → R4, IsSmoothDiskEmbedding e ∧ e '' closedUnitDisk ⊆ energySurface H ∧
    e '' unitCircle = P.image

/-- An open book decomposition of `S` with disk-like pages and binding `P`, adapted
to the flow (Definition 1.2). Pages are `page θ (closed disk)`, `θ ∈ ℝ/ℤ`:
1. the page family is smooth in `(θ, u)` and `1`-periodic in `θ`;
2. every page is a disk-like global surface of section bounded by `P`;
3. every boundary circle runs along `P` in the flow direction:
   `page θ (cos 2πt, sin 2πt) = x(Tt)` (binding orientation = orientation of `P`);
4. pages are positively oriented by `dλ₀ = ω₀`;
5. `(θ, u) ↦ page θ u` maps `[0, 1) × (open disk)` bijectively onto `S \ x(ℝ)`, with
   injective differential (so `θ` is a smooth fibration `S \ x(ℝ) → ℝ/ℤ`). -/
structure AdaptedDiskOpenBook (H : R4 → ℝ) (P : PeriodicOrbit H) where
  page : ℝ → Plane → R4
  smooth : ContDiff ℝ ∞ (fun z : ℝ × Plane => page z.1 z.2)
  periodic : ∀ θ u, page (θ + 1) u = page θ u
  page_section : ∀ θ, IsDiskLikeGlobalSectionMap H P (page θ)
  binding : ∀ θ t, page θ (circlePoint t) = P.x (P.T * t)
  page_positive : ∀ θ, ∀ u ∈ openUnitDisk,
    0 < omega0 (fderiv ℝ (page θ) u (Pi.single 0 1)) (fderiv ℝ (page θ) u (Pi.single 1 1))
  fibration : ∀ y ∈ energySurface H, y ∉ P.image →
    ∃! z : ℝ × Plane, z.1 ∈ Set.Ico (0 : ℝ) 1 ∧ z.2 ∈ openUnitDisk ∧ page z.1 z.2 = y
  regular : ∀ θ : ℝ, ∀ u ∈ openUnitDisk,
    Function.Injective (fderiv ℝ (fun z : ℝ × Plane => page z.1 z.2) (θ, u))

/-- `P` is the binding of an adapted open book decomposition with disk-like pages. -/
def HasAdaptedDiskOpenBook (H : R4 → ℝ) (P : PeriodicOrbit H) : Prop :=
  Nonempty (AdaptedDiskOpenBook H P)

end

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. 1 (global surface of section), p. 2 (open book decomposition, Definition 1.2), p. 3 (unknotted)

Read-back

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

Read-back: `Def_HryniewiczCriterion_GlobalSection`

Namespace HryniewiczCriterion; uses Def_HryniewiczCriterion_Basic: $\mathbb R^4$ with coordinates $x_0,\dots,x_3$ ; $\omega_0(u,v)=u_0v_1-u_1v_0+u_2v_3-u_3v_2$ ; $X_H(x)=(-\partial_1H,\partial_0H,-\partial_3H,\partial_2H)(x)$ (zero where $H$ is not differentiable); $\Sigma_H=\{H=1\}$ ; trajectories are curves $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$ ; a periodic orbit $P=(x_P,T_P)$ is a trajectory with a positive (not necessarily minimal) period $T_P$ ; $\operatorname{im}P=x_P(\mathbb R)$ . $H:\mathbb R^4\to\mathbb R$ is arbitrary throughout.

`Plane`, `closedUnitDisk`, `openUnitDisk`, `unitCircle`

Plane is $\mathbb R^2$ with coordinates $(u_0,u_1)$ (built-in sup norm; irrelevant for derivatives).

\bar D=\{u_0^2+u_1^2\le1\},\qquad D=\{u_0^2+u_1^2<1\},\qquad S^1=\{u_0^2+u_1^2=1\}.

`circlePoint`

c(t)=\bigl(\cos 2\pi t,\ \sin 2\pi t\bigr)\in S^1,\qquad t\in\mathbb R,

traversing $S^1$ once counter-clockwise (in the $(u_0,u_1)$ orientation) as $t$ runs over $[0,1]$ .

`IsSmoothDiskEmbedding`

A map $e:\mathbb R^2\to\mathbb R^4$ qualifies iff

$e$ is $C^\infty$ on all of $\mathbb R^2$ ;
$e$ is injective on $\bar D$ ;
for every $u\in\bar D$ the derivative $De_u:\mathbb R^2\to\mathbb R^4$ is injective.

`IsDiskLikeGlobalSectionMap`

For $H$ , a periodic orbit $P$ and $e:\mathbb R^2\to\mathbb R^4$ , all of:

$e$ is a smooth disk embedding (above);
$e(\bar D)\subseteq\Sigma_H$ ;
$e(S^1)=\operatorname{im}P$ (equality of sets; no orientation, parametrisation or degree condition on $e|_{S^1}$ );
for every $u\in D$ (open disk): $X_H(e(u))\notin\operatorname{range}(De_u)$ — the vector field is not tangent to the image of the derivative at interior points (nothing is required at boundary points, and no co-orientation/sign is imposed);
for every trajectory $y$ of $H$ with $y(0)\notin\operatorname{im}P$ , and every $a\in\mathbb R$ : there exists $t>a$ with $y(t)\in e(\bar D)$ , and there exists $t<a$ with $y(t)\in e(\bar D)$ . Equivalently, the set of hitting times $\{t: y(t)\in e(\bar D)\}$ is unbounded above and unbounded below. Hits are counted in the closed image $e(\bar D)$ , which includes the boundary $\operatorname{im}P$ .

`BoundsDiskLikeGlobalSection`

\exists\, e:\mathbb R^2\to\mathbb R^4\ \text{such that } e \text{ is a disk-like global section map for } (H,P).

`IsUnknotted`

There exists $e:\mathbb R^2\to\mathbb R^4$ which is a smooth disk embedding with $e(\bar D)\subseteq\Sigma_H$ and $e(S^1)=\operatorname{im}P$ . (Only conditions 1–3 above; no transversality and no return condition. The spanning disk must lie inside $\Sigma_H$ .)

`AdaptedDiskOpenBook` (structure)

Data: a map $\mathrm{page}:\mathbb R\times\mathbb R^2\to\mathbb R^4$ , written $p_\theta(u)$ , subject to:

smooth: $(\theta,u)\mapsto p_\theta(u)$ is $C^\infty$ on $\mathbb R\times\mathbb R^2$ ;
periodic: $p_{\theta+1}(u)=p_\theta(u)$ for all $\theta\in\mathbb R$ , $u\in\mathbb R^2$ ;
page_section: for every $\theta\in\mathbb R$ , $p_\theta$ is a disk-like global section map for $(H,P)$ (conditions 1–5 above);
binding: for all $\theta,t\in\mathbb R$ :

p_\theta\bigl(c(t)\bigr)=x_P(T_P\,t),

so every page restricted to the circle is the same map, and the counter-clockwise boundary circle is sent onto the orbit with one turn of the circle corresponding to time $T_P$ ;

page_positive: for every $\theta$ and every $u\in D$ :

\omega_0\Bigl(\partial_{u_0}p_\theta(u),\ \partial_{u_1}p_\theta(u)\Bigr)>0 ;

fibration: for every $y\in\Sigma_H$ with $y\notin\operatorname{im}P$ there is exactly one pair $(\theta,u)$ with $\theta\in[0,1)$ , $u\in D$ and $p_\theta(u)=y$ ;
regular: for every $\theta\in\mathbb R$ and $u\in 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.

Consequence of the fields as written: injectivity of $p_\theta$ on $\bar D$ (from page_section) combined with binding forces $t\mapsto x_P(T_Pt)$ to be injective on $[0,1)$ , i.e. $x_P$ is injective on $[0,T_P)$ . Nothing requires $\Sigma_H\setminus\operatorname{im}P$ to be nonempty, and no condition is stated relating the pages to $\Sigma_H$ beyond page_section (images in $\Sigma_H$ ) and fibration.

`HasAdaptedDiskOpenBook`

$(H,P)$ has an adapted disk open book iff at least one structure AdaptedDiskOpenBook for $(H,P)$ exists.

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

Disk-like global surfaces of section, unknots, adapted open books

Read-back: Def_HryniewiczCriterion_GlobalSection

Plane, closedUnitDisk, openUnitDisk, unitCircle

circlePoint

IsSmoothDiskEmbedding

IsDiskLikeGlobalSectionMap

BoundsDiskLikeGlobalSection

IsUnknotted

AdaptedDiskOpenBook (structure)

HasAdaptedDiskOpenBook