Let H:R4→R be smooth with S=H−1(1) strictly star-shaped, and assume the Hamiltonian flow of XH on S, a positive reparametrization of the Reeb flow of λ0∣S, is dynamically convex. Then for every prime periodic orbit Pˉ on S,
Pˉbounds a disk-like global surface of section⟺Pˉis unknotted andsl(Pˉ)=−1.
No non-degeneracy assumption is made. The criterion reduces the existence of a disk-like global section, a global dynamical property, to a topological check on the orbit.
Formalization Note Hryniewicz states the theorem for any dynamically convex contact form on S3. Such a form is tight, and every tight contact form on S3 is diffeomorphic to λ0∣S on a star-shaped S (Eliashberg). That reduction is not part of this statement; Hryniewicz makes the same reduction at the start of Section 3. The flow is that of XH, which has the same orbits, global sections, unknots, self-linking numbers and indices as the Reeb flow.
namespace HryniewiczCriterion
/-- Hryniewicz's criterion (Theorem 1.7): for a dynamically convex flow on a strictly
star-shaped energy surface in `ℝ⁴`, a prime periodic orbit bounds a disk-like global
surface of section if and only if it is unknotted and has self-linking number `-1`. -/
theorem hryniewicz_criterion (H : R4 → ℝ)
(hS : IsStrictlyStarShapedLevel H) (hdc : IsDynamicallyConvex H)
(P : PeriodicOrbit H) (hP : P.IsPrime) :
BoundsDiskLikeGlobalSection H P ↔ IsUnknotted H P ∧ HasSelfLinkingNumber H P (-1) := 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, Theorem 1.7, p. 3, first sentence
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Read-back: hryniewicz_criterion
Binders and hypotheses. Let H:R4→R be any function, and assume:
(hS) the level Σ=H−1(1) is a strictly star-shaped level of H (H is C∞, each ray from the origin meets Σ exactly once, and DH(x)x>0 on Σ);
(hdc)H is dynamically convex (every periodic orbit, of every period, with every linearized flow, has index μ≥3; see below);
P is a periodic orbit of XH on Σ (a trajectory xP with a period TP>0);
(hP)P is prime: xP(t)=xP(0) for 0<t<TP.
Conclusion (an equivalence).
(P bounds a disk-like global section)⟺(P is unknotted and P has self-linking number −1),
where:
left side: there exists e:R2→R4, C∞, injective with injective derivative on D, with e(D)⊆Σ, e(S1)=imP, XH(e(u))∈/rangeDe(u) for all u in the open disk D, and such that every trajectory y with y(0)∈/imP meets e(D) at some time >a and at some time <a, for every a∈R;
right side, first part: there exists a C∞e:R2→R4, injective with injective derivative on D, with e(D)⊆Σ and e(S1)=imP;
right side, second part: there is ε0>0 such that for every ε∈(0,ε0) the loops
have linking number −1 (some unit N avoided by both loops on R exists, and for every such N the Gauss integral GN(ℓP,ℓPε)=−1).
Edge cases. The left side contains no orientation condition and no condition on the direction of the boundary orbit; the self-linking number on the right is computed with the specific frame vector ξ1 and with the given parametrization s↦xP(TPs), s∈[0,1]. Both directions of the equivalence are asserted under (hS), (hdc), (hP).
Unfolded definitions used above
Throughout, R4 is the space of functions {0,1,2,3}→R (with the sup norm as its normed-space structure), points are written x=(x0,x1,x2,x3), and R2 (points u=(u0,u1)) is likewise {0,1}→R. DH(x) denotes the Fréchet derivative of H at x, which is by convention the zero map wherever H is not differentiable; similarly for every other derivative below. Divisions by 0 and inverses of 0 evaluate to 0.
Euclidean inner product and norm: ⟨x,y⟩=∑i=03xiyi, ∣x∣=⟨x,x⟩.
Partial derivatives ∂iH(x)=DH(x)ei (ei the i-th standard basis vector), and the Hamiltonian vector field
XH(x)=(−∂1H(x),∂0H(x),−∂3H(x),∂2H(x)).
Energy surface Σ={x∈R4:H(x)=1}.
Strictly star-shaped level (hypothesis hS): (i) H:R4→R is C∞ on all of R4; (ii) for every u=0 there is exactly one r>0 with H(ru)=1; (iii) for every x with H(x)=1, DH(x)x>0. (Consequence of (iii): H(0)=1, so 0∈/Σ, and XH=0 on Σ.)
Trajectory: a map y:R→R4 that is differentiable at every t∈R with y′(t)=XH(y(t)), and with H(y(t))=1 for all t∈R.
Periodic orbitP: a pair (xP,TP) consisting of a trajectory xP:R→R4 and a number TP>0 with xP(t+TP)=xP(t) for all t. TP is a period, not necessarily the minimal one; the same geometric orbit gives many different P (any time shift, any positive multiple of the minimal period). Its image is imP={xP(t):t∈R}.
Prime: xP(t)=xP(0) for all 0<t<TP (i.e. TP is the minimal period).
Two fixed linear maps Q1(x)=(−x2,x3,x0,−x1) and Q2(x)=(x3,x2,−x1,−x0), and the frame vectors
Given a path of real 2×2 matrices φ:R→M2(R) and s∈R, an angle lift from s is a function θ:R→R, continuous on [0,1], with θ(0)=s, such that for every t∈[0,1] there is r>0 with φ(t)ρ(s)=rρ(θ(t)). (No continuity or invertibility of φ is assumed; if φ(t)ρ(s)=0 for some t∈[0,1], no lift from s exists.)
Winding set W(φ)={2πθ(1)−s:s∈[0,2π],θ an angle lift of φ from s}⊆R.
Index: let a=infW(φ), b=supW(φ) (each set to 0 if W(φ) is empty or unbounded on that side), and k=⌈b⌉ (least integer ≥b). Then
μ(φ)={2(k−1)2k−1if a≤k−1,otherwise.
In particular, if W(φ)=∅ then a=b=0, k=0 and μ(φ)=−1.
A linearized flow along a curve x:R→R4 is a map Y:R→L(R4,R4) (continuous linear maps) with Y(0)=Id and, for every t∈R, Y differentiable at t with Y′(t)=DXH(x(t))∘Y(t), where DXH is the Fréchet derivative of the vector field XH.
Projection along XH: πx(v)=v−λx(XH(x))λx(v)XH(x).
H is dynamically convex means: for every periodic orbit P (any period TP, so including all multiple covers and time shifts) and every linearized flow Y along xP, μ(ΦP,Y)≥3. (If for some P no linearized flow exists, the condition is vacuous for that P.)
Disks and global sections.
D={u:u02+u12≤1}, D={u:u02+u12<1}, S1={u:u02+u12=1}, and c(t)=(cos2πt,sin2πt).
Smooth disk embeddinge:R2→R4: e is C∞ on all of R2, injective on D, and De(u) is injective for every u∈D.
Disk-like global section map for (H,P): a map e:R2→R4 such that
e is a smooth disk embedding;
e(D)⊆Σ;
e(S1)=imP (set equality);
for every u∈D (open disk), XH(e(u))∈/rangeDe(u);
for every trajectory y with y(0)∈/imP and every a∈R, there exist t>a with y(t)∈e(D) and t′<a with y(t′)∈e(D) (the hitting set is the image of the closed disk).
No orientation condition is imposed.
P bounds a disk-like global section: some disk-like global section map for (H,P) exists.
P is unknotted: there is a smooth disk embedding e with e(D)⊆Σ and e(S1)=imP (conditions 1–3 above only).
Adapted disk open book for (H,P): a map F:R×R2→R4, F(ϑ,u)=Fϑ(u), such that
F is jointly C∞;
Fϑ+1=Fϑ for all ϑ;
every page Fϑ is a disk-like global section map for (H,P);
(binding) Fϑ(c(t))=xP(TPt) for all ϑ,t∈R;
(positivity) for all ϑ and u∈D, ω0(∂u0Fϑ(u),∂u1Fϑ(u))>0;
(fibration) every y∈Σ∖imP equals F(ϑ,u) for exactly one pair (ϑ,u) with ϑ∈[0,1), u∈D;
(regularity) for all ϑ∈R and u∈D, the derivative DF(ϑ,u):R×R2→R4 is injective.
"P has an adapted disk open book" means such an F exists. (Since each page is injective on D, the binding condition forces t↦xP(TPt) to be injective on [0,1), i.e. P prime.)
Linking and self-linking.
ν(x)=x/∣x∣ (with ν(0)=0).
For N∈R4, the map σN(y)=1−⟨y,N⟩y−⟨y,N⟩N (equal to 0 when ⟨y,N⟩=1), with values in R4.
volN(a,b,c)=det of the 4×4 matrix with rows −N,a,b,c.
Gauss integral of two curves γ1,γ2:R→R4 with respect to N: writing α(s)=σN(γ1(s)), β(t)=σN(γ2(t)),
where derivatives are 0 at non-differentiability points, the integrand is 0 where α(s)=β(t), and an interval integral of a non-integrable function is 0.
γ1,γ2 have linking number n∈Z: (a) there exists N with ∣N∣=1 such that γ1(s)=N and γ2(s)=N for all s∈R; and (b) for everyN with ∣N∣=1 avoiding both curves on all of R in that sense, GN(γ1,γ2)=n. (Avoidance is required over all s∈R; the integral uses only [0,1]. The curves are not required to be closed or smooth.)
Orbit loop ℓP(s)=ν(xP(TPs)); push-off loop ℓPε(s)=ν(xP(TPs)+εξ1(xP(TPs))). Over s∈[0,1] these traverse the period TP, which is the minimal period only if P is prime.
P has self-linking number n: there is ε0>0 such that for every ε∈(0,ε0), the curves ℓP,ℓPε have linking number n (in the sense above).
P links Q nontrivially: there is an integer n=0 such that ℓP,ℓQ have linking number n.
Confirmed by the moderator at approval.