Open book decompositions with pages projected from fast finite-energy planes
OpenFiniteEnergyPlane.exists_fastPlane_open_bookLet have a strictly star-shaped level (in the sense of HryniewiczCriterion), the same function on , a smooth -compatible complex structure on , and a periodic Reeb orbit of with . Suppose every periodic Reeb orbit of period at most is nondegenerate, is smaller than every such period and than every difference of two distinct such periods, and is sequentially compact in for every compact with . If there is an embedded fast finite-energy plane asymptotic to at , then for every there is a map , -periodic in the first variable, such that
- every is an embedded fast finite-energy plane asymptotic to at ;
- avoids , maps bijectively onto , has injective derivative, and is Reeb positive (
IsPlaneOpenBook); - every Reeb trajectory with meets at times larger than any given and at times smaller than any given , for every .
Formalization Note The level is given in the form of exists_transverse_disk_open_book_of_approx and of the goal of the previous mission. Periods are those of ReebOrbit H (not necessarily minimal, so multiple covers count). The hypothesis on is exactly the conclusion of isSeqCompact_embeddedFastPlaneSet for the same , quantified over ; the cylinder is the cone . is P.IsCZAtLeast 3, the index of the linearized flow along in the global frame of . Hryniewicz writes and restricts to ; on a strictly star-shaped level has a global frame, which extends over every capping disk, so the index depends only on , , and the condition is not restated. Hryniewicz assumes every contractible orbit nondegenerate; only orbits of period at most appear here. Clause 3, together with transversality of the leaves to the Reeb field (isFastPlane_immersion_transverse), is the statement that each page is a global surface of section. The given plane is a hypothesis only; the theorem does not assert that it is a page, nor does Hryniewicz's Theorem 2.5. See FiniteEnergyPlane_OpenBook for "orientation preserving" and the period.
import Definitions.Def_FiniteEnergyPlane_OpenBook
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hryniewicz (Trans. AMS 2012), Theorem 2.5, for a strictly star-shaped level `S = H⁻¹(1) ⊂ ℝ⁴` (in
the coordinates of `HryniewiczCriterion`) and a compatible complex structure `J` on `ξ`. Let `P` be
a periodic Reeb orbit of Conley–Zehnder index at least `3` such that every periodic orbit of period
at most `P.T` is nondegenerate; let `0 < γ` be smaller than every such period and every difference
of two distinct such periods, and suppose `Λ(K, P)` is sequentially compact in `C^∞_loc` for every
compact `K ⊂ V 1 \ {0}` disjoint from the cone `ℝ × x(ℝ)`. If there is an embedded fast
finite-energy plane asymptotic to `P` at `∞`, then for every `l ≥ 1` there is a `C^l` map
`U : ℝ × ℂ → V 1`, `1`-periodic in the first variable, such that
(1) every `U(θ, ·)` is an embedded fast finite-energy plane asymptotic to `P` at `∞`;
(2) `pageMap H U` avoids `x(ℝ)`, maps `[0, 1) × ℂ` bijectively onto `S \ x(ℝ)`, has injective
derivative, and is positive against the Reeb field (`IsPlaneOpenBook`);
(3) every Reeb trajectory `y` with `y 0 ∉ x(ℝ)` meets every leaf `pageMap H U (θ, ·)` at times larger
than any given `n` and at times smaller than any given `n`. -/
theorem exists_fastPlane_open_book (H₀ : HryniewiczCriterion.R4 → ℝ)
(hH₀ : HryniewiczCriterion.IsStrictlyStarShapedLevel H₀) :
let H : V 1 → ℝ := fun y => H₀ (fun k => y (Fin.cast (by norm_num) k))
∀ J : V 1 → V 1 →L[ℝ] V 1, IsCompatibleXiStructure H J → ∀ P : ReebOrbit H,
P.IsCZAtLeast 3 → (∀ Q : ReebOrbit H, Q.T ≤ P.T → Q.IsNondegenerate) →
∀ γ : ℝ, 0 < γ → (∀ Q : ReebOrbit H, Q.T ≤ P.T → γ < Q.T) →
(∀ Q₁ Q₂ : ReebOrbit H, Q₁.T ≤ P.T → Q₂.T ≤ P.T → Q₁.T ≠ Q₂.T → γ < |Q₁.T - Q₂.T|) →
(∀ K : Set (V 1), IsCompact K → (0 : V 1) ∉ K → (∀ y ∈ K, proj H y ∉ Set.range P.x) →
IsSeqCompactCInftyLoc (embeddedFastPlaneSet H J P K γ)) →
∀ u₀ : ℂ → V 1, IsFastPlane H J u₀ → IsNondegenerateEnd H u₀ cylInf P 1 → IsEmbeddedPlane u₀ →
∀ l : ℕ, 1 ≤ l → ∃ U : ℝ × ℂ → V 1, IsPlaneOpenBook H J P l U ∧
∀ y : ℝ → V 1, IsReebTrajectory H y → y 0 ∉ Set.range P.x → ∀ θ n : ℝ,
(∃ t > n, y t ∈ Set.range (fun z => pageMap H U (θ, z))) ∧
(∃ t < n, y t ∈ Set.range (fun z => pageMap H U (θ, z))) := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
FiniteEnergyPlane.exists_fastPlane_open_book
Let (with indexed by coordinates ) satisfy: ; for every there is exactly one with ; and whenever . Let be read on via the identity relabelling of coordinates; below, and are identified, and .
Then, for every that is a compatible -structure for ; every Reeb orbit of with "CZ index of at least "; such that every Reeb orbit of with recorded period is nondegenerate; for every with
- ,
- for every Reeb orbit with ,
- for all Reeb orbits with and ,
and such that the following compactness hypothesis holds:
for every compact with and with for all , the set is sequentially compact;
for every that is a fast plane, has end on , and is an embedded plane; and for every with : there exists with the two properties below, where .
(A) is a plane open book for :
- is on all of ;
- for all ;
- for every , is a fast plane, has end on , and is an embedded plane;
- for every ;
- for every with and there is exactly one with and ;
- is injective for every ;
- for every there are , with .
(B) for every Reeb trajectory with and all , there exist and with
may depend on all the quantified data, including , and . The statement asserts no relation between and (for instance, is not asserted to be a page), and no -energy or base point of the pages of . The compactness hypothesis, the "CZ at least " condition, the nondegeneracy of orbits of period at most and the bounds on are all assumptions of the statement, are not derived, and the statement does not say whether they can be jointly satisfied. Orbits with recorded period larger than are not subject to any hypothesis.
Background notions
Conventions. with coordinates ; below mostly , so . denotes the real Fréchet derivative, which is the zero map by convention where is not differentiable. For on : , . Also , and is the image of .
Symplectic data on . for even, for odd. . . has components ; .
Reeb field. (the zero vector where ). -membership: "" means and .
Strictly star-shaped level. ; for every there is exactly one with ; and whenever . The last clause forces .
Compatible -structure. is on all of , and for all with and all : ; ; if then ; .
Radial coordinates. is a chosen with if one exists, and otherwise. and . (For star-shaped : at the is unique; at the value is .)
Almost complex structure on . For with , , set , , and . Then
Finite energy curve on (only itself is used here). with: ; for all ; is differentiable at each with ; and , where
with , , the supremum over monotone (non-decreasing) , and the positive part (the integral is a -valued Lebesgue integral).
-energy. For : , with .
Reeb orbit. A Reeb orbit of is a pair with , , , and for all . is any positive period, not necessarily the minimal one, so covers are orbits. is prime when for all .
Reeb trajectory. Any such that for every : and is differentiable at with . Nothing excludes from being periodic or from running along a Reeb orbit.
Nondegenerate orbit. For every with and for all , and every : implies . (Vacuous if no such exists.)
Nondegenerate end at infinity on (with sign ; written " has end on "). There exist reals and such that, as and uniformly in ,
Fast plane. such that:
- is a finite energy curve on ;
- there exists a prime Reeb orbit of on which has an end in the above sense;
- with and , the zero set of is finite, and there are integers , , summing to , such that for each there is with on and, for each , the loop has winding number .
Here a loop "has winding number " when is continuous, -periodic, nowhere zero, and there is a continuous with and . An empty satisfies clause 3; the definition allows nonempty with indices of mixed sign summing to .
The coordinate is
for , with the Euclidean norm, and .
Embedded plane. is injective and is an injective linear map for every .
Set of embedded fast planes (, ). All that are fast planes, have end on , are embedded planes, have , and satisfy
When this says the energy on is . is not itself required to be prime; the prime orbit of the fast plane condition is a separate existential.
convergence on . means: for every compact and every , the -th iterated Fréchet derivatives of converge uniformly on to that of .
Sequential compactness of a set of maps . Every sequence in has a subsequence (strictly increasing reindexing) converging in on to some element of . The empty set has this property.
Hypothesis "CZ index of is at least " (for a Reeb orbit of , ). Identify with and let be any periodic orbit of for the Hamiltonian field: , , , , , where . Then, for every such with the same image as and with action , and for every with , , one has . Here has entries
with the real pair , , , and at . The integer is: let be the set of numbers over and continuous on with and for some for each ; let , (with the convention that both equal if is empty, and each equals if unbounded on its side). Then if , and otherwise. The hypothesis is universally quantified over and and so is vacuous if no such pair exists.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.