The -projected outward conormal of a disk transverse to the flow winds once relative to the global frame
ProvedHryniewiczCriterion.disk_conormal_xi_winding_eq_oneLet be strictly star-shaped, a prime periodic orbit, and a smooth embedding of the closed unit disk into with and for . Let be a smooth -periodic lift with . Let be the outward conormal of the disk along its boundary, and let
be its projection to along . Then at , with smooth -periodic and smooth satisfying
That is, the conormal winds exactly once, positively, relative to the global frame of , where .
Proof idea: is intrinsic to the disk, so we may reflect to make . Transversality makes the projection along an orientation-preserving isomorphism over the open disk. The frame extends over the disk, so it has winding relative to , and the radial vector winds . At the boundary, , so up to . By Stokes, the boundary orientation matches the flow direction.
import Definitions.Def_HryniewiczCriterion_GlobalSection import Definitions.Def_HryniewiczCriterion_SelfLinking open HryniewiczCriterion open scoped ContDiff
theorem HryniewiczCriterion.disk_conormal_xi_winding_eq_one (H : R4 → ℝ) (hS : IsStrictlyStarShapedLevel H) (P : PeriodicOrbit H) (hP : P.IsPrime)
(e : Plane → R4) (he : IsSmoothDiskEmbedding e)
(hDS : e '' closedUnitDisk ⊆ energySurface H) (hbd : e '' unitCircle = P.image)
(htr : ∀ u ∈ openUnitDisk, hamiltonianVectorField H (e u) ∉ Set.range (fderiv ℝ e u))
(u : ℝ → Plane) (hu : ContDiff ℝ ∞ u) (huper : ∀ s, u (s + 1) = u s)
(hucirc : ∀ s, u s ∈ unitCircle) (heu : ∀ s, e (u s) = P.x (P.T * s)) :
∃ r θ : ℝ → ℝ, ContDiff ℝ ∞ r ∧ ContDiff ℝ ∞ θ ∧ (∀ s, 0 < r s) ∧ (∀ s, r (s + 1) = r s) ∧
(∀ s, θ (s + 1) = θ s + 2 * Real.pi) ∧
∀ s, (fderiv ℝ e (u s) (u s) - (liouvilleForm (P.x (P.T * s)) (fderiv ℝ e (u s) (u s)) / liouvilleForm (P.x (P.T * s)) (hamiltonianVectorField H (P.x (P.T * s)))) • hamiltonianVectorField H (P.x (P.T * s))) =
r s • (Real.cos (θ s) • xiFrame1 H (P.x (P.T * s)) + Real.sin (θ s) • xiFrame2 H (P.x (P.T * s))) := by sorry