Embedded fast planes with the same image differ by an affine reparametrization and a translation
OpenFiniteEnergyPlane.exists_shiftA_comp_affine_of_range_eqLet be a strictly star-shaped level and a smooth -compatible complex structure on . Let be a periodic Reeb orbit with ( may be degenerate) and let and be embedded fast finite-energy planes asymptotic to at with . Then there are and with such that for all .
Formalization Note The puncture at is IsNondegenerateEnd H u cylInf P 1 (nondegenerate in the sense of Hryniewicz 2014, Definition 2.9); "fast" is IsFastPlane, "embedded" is IsEmbeddedPlane. is P.IsCZAtLeast 3, the index of the linearized flow along in the global frame of ; itself need not be nondegenerate. Hryniewicz writes the hypothesis as , where is the index of in the class of trivializations of along that extend over the capping disk . On a strictly star-shaped level has a global frame, which extends over every capping disk, so is determined by and equals the index in that frame. The translation is shiftA c v, . Hryniewicz's assumption holds for any two planes asymptotic to on a strictly star-shaped level (global frame of ) and is not restated. Of Hryniewicz's dichotomy (equal or disjoint images), only the case of equal images is stated here.
import Definitions.Def_FiniteEnergyPlane_Fredholm
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hryniewicz (Trans. AMS 2012), Lemma 6.25. Let `u` and `v` be embedded fast finite-energy planes
asymptotic to the same orbit `P` at `∞`, where the Conley–Zehnder index of `P` is at least `3`. If
`proj H ∘ u` and `proj H ∘ v` have the same image, then `u` and `v` differ by an affine
reparametrization and a translation in the symplectization: `u(Az + B) = (c · v)(z)` for all `z`,
for some `c ∈ ℝ` and `A, B ∈ ℂ` with `A ≠ 0`. -/
theorem exists_shiftA_comp_affine_of_range_eq (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
(J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J)
(P : ReebOrbit H) (hcz : P.IsCZAtLeast 3) (u v : ℂ → V 1)
(hu : IsFastPlane H J u) (huP : IsNondegenerateEnd H u cylInf P 1)
(hue : IsEmbeddedPlane u)
(hv : IsFastPlane H J v) (hvP : IsNondegenerateEnd H v cylInf P 1) (hve : IsEmbeddedPlane v)
(hrange : Set.range (proj H ∘ u) = Set.range (proj H ∘ v)) :
∃ (c : ℝ) (A B : ℂ), A ≠ 0 ∧ ∀ z, u (A * z + B) = shiftA c v z := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
FiniteEnergyPlane.exists_shiftA_comp_affine_of_range_eq
Statement. Let be a Hamiltonian with strictly star-shaped level , let be a compatible structure on , let be a Reeb orbit of with image satisfying the Conley–Zehnder bound , and let be two maps such that, for each ,
- is a fast plane for ;
- has a nondegenerate end at infinity at the same orbit , i.e. ;
- is embedded;
and such that as subsets of . Then there exist and with such that for every ,
Here is ordinary scalar multiplication of the vector . For one has and . The numbers are only asserted to exist, not to be unique. is not assumed prime. The prime orbit in the definition of "fast plane" is existentially quantified separately for and for and is not stated to equal . The Conley–Zehnder bound is a statement about only, and it may hold vacuously as described below.
Meaning of every symbol used above
Ambient space and linear structures. has coordinates . The fixed linear maps and forms are
where is the Euclidean dot product.
The Hamiltonian (hypothesis "strictly star-shaped level"). is ; for every there is exactly one with ; and at every with . Write . Nothing is assumed about . Further notation:
- is the vector of partial derivatives, ;
- the Reeb field is , with the convention (so wherever );
- .
The structure (hypothesis "compatible on "). is , and for every and all :
No condition is imposed on outside , nor for .
Radial coordinates. For let be a (chosen) with if such an exists, and otherwise; for this is the unique one from the star-shapedness hypothesis. Put
For , is the point of on the ray through and ; always .
The Reeb orbit . consists of a map and a number such that , and for all . The period is not required to be the minimal period. Its image is . A Reeb orbit is called prime if for all .
The almost complex structure on . For let , , and define the linear forms and (division by gives ). Then
Plane coordinates. For and , and , where is the real derivative (taken to be where is not differentiable). For a map write and .
Finite-energy curve on . is on ; for every ; at every , is differentiable and ; and , where
the supremum ranging over all , nondecreasing (the integral is the Lebesgue integral of the nonnegative part).
Nondegenerate end at infinity at an orbit (written ). With , there exist and such that, as , uniformly in ,
("Uniformly" means: for every there is with the quantity at most in absolute value/norm for all and all .)
The function . For define and with , and the Euclidean norm (again ), and the complex coordinate . Then
Winding of a loop. A map has winding if is continuous, -periodic, nowhere zero, and there is a continuous with for all and .
Fast plane. is a fast plane if all three hold:
- is a finite-energy curve on ;
- there exists some prime Reeb orbit (not necessarily equal to ) with ;
- the zero set is finite, and there are integers () with such that for each there is with on the closed disc minus , and for every the loop has winding . (If is empty this condition holds automatically.)
Embedded plane. is called embedded if is injective and, for every , the real-linear map is injective. (This is a condition on itself, not on .)
Conley–Zehnder bound . This hypothesis says: for all of the following data:
- every and with , and for all ( not necessarily minimal),
- such that and ,
- and every with and for all .
If no such exists, the hypothesis holds vacuously. The quantity is computed from the real matrix path
where and (division by gives ). Let be the set of numbers over all and all continuous on with such that for each , is a positive multiple of . With , (both taken to be if is empty or unbounded on that side),
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.