Planar circular restricted three-body dynamics and rational global sections

Definition

BirkhoffGlobalSection

by Yivy Yu · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

celestial-mechanicsdynamical-systemshamiltonian-dynamics

This module fixes the formal objects for one labeled primary in the planar circular restricted three-body problem.

The Jacobi and Levi-Civita formulas are total real-valued Lean functions. They agree with Joung--van Koert equations (1.1) and (2.2) on their physical domains; the separate predicates collisionFree and secondCollisionDistanceSq > 0 record where the source Hamiltonians are nonsingular. A critical point requires both Fréchet differentiability and zero derivative. firstCriticalValue is only an infimum by definition; a separate theorem goal identifies it with $H_\mu(L_1)$ for $0<\mu<1$ .

The regularized component $\Sigma_{\mu,c}$ is the connected component based at the collision over $q=(-\mu,0)$ . The flow predicates record the Hamiltonian generator and compatibility with the antipodal deck map $(z,w)\mapsto(-z,-w)$ .

The module deliberately distinguishes two meanings of “retrograde.” Under the free invariant covering and flow-equivariance hypotheses used by the mission, AntipodalPeriodicTrajectory represents a prime noncontractible quotient orbit by a point in the Levi-Civita cover and its quotient period $P$ : the lift reaches its antipode at time $P$ , and no earlier positive time reaches either candidate lift. IsGeometricBirkhoffRetrogradeTrajectory records the geometric orbit used in the Birkhoff-conjecture formulation. Its Jacobi projection has the $q_2$ -reflection symmetry and, over the quotient period, is a simple collision-free loop with winding $+1$ about the chosen primary. The continuous polar lift permits temporary angular reversal. antipodalTrajectoryDoubleLift traverses this trajectory twice to form the closed Levi-Civita orbit used as the page boundary.

IsAstronomicallyRetrogradeOrbit instead requires strict positivity at every time of the Joung--van Koert Proposition 2.2 expression

(q_1+\mu)p_2-q_2p_1-\mu(q_1+\mu).

This is their sufficient pointwise test for increasing sidereal angle and is a priori stronger than Birkhoff's usage (Joung--van Koert, Remark 2.3). The analogous strict negative predicate records direct motion.

DiskLikeGlobalSurfaceOfSection describes an ordinary smooth embedded disk in the Levi-Civita component. Its interior is transverse to the Hamiltonian vector field, its boundary is the binding orbit, and every nonbinding trajectory returns to its interior at arbitrarily large positive and negative times, matching Hryniewicz Definition 1.1.

For the rational page, the module constructs the topological antipodal quotient

Q_{\mu,c}=\Sigma_{\mu,c}/(s\sim -s)

and descends every time map with Quotient.map; antipodal flow equivariance makes this representative-independent. Joint continuity and the identity and composition laws of the descended action are required explicitly. RationalDiskLikeGlobalSurfaceOfSection also requires the component action to be invariant and free and the quotient binding to have prime period equal to half the recorded period of its closed lift. A quotient page is induced by a smooth immersive disk lift. Its interior is a topological embedding, its boundary image is the prime quotient orbit, and its only nontrivial fibers are the antipodal pairs on the boundary. This gives the exact two-fold boundary map of a rational $2$ -disk. Because no smooth-manifold structure is installed on the quotient type, smoothness and transversality are deliberately expressed on the Levi-Civita lift. The global returns are stated directly in the quotient at arbitrarily late and early times. The predicate asserts one rational global surface of section; it does not assert an open-book fibration or an explicit coordinate equivalence with Moser regularization.

Finally, HasPositiveTangentialHessianOn requires $C^2$ regularity and positivity of the second directional derivative on every nonzero vector annihilated by the first derivative. It records one differential clause of Joung--van Koert Proposition 4.4, not the full geometric definition of a convex body.

Definition code

import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Dynamics.Flow
import Mathlib.Topology.Connected.Basic
import Mathlib.Topology.Maps.Basic

namespace BirkhoffGlobalSection

noncomputable section

open scoped ContDiff

/-- Four real coordinates, ordered as `(q₁,q₂,p₁,p₂)` for the Jacobi Hamiltonian
and as `(z₁,z₂,w₁,w₂)` after Levi-Civita regularization. -/
abbrev Phase := Fin 4 → ℝ

/-- Two real coordinates, used for the parameter disk of a global section. -/
abbrev Plane := Fin 2 → ℝ

def qNormSq (s : Phase) : ℝ := s 0 ^ 2 + s 1 ^ 2

def zNormSq (s : Phase) : ℝ := s 0 ^ 2 + s 1 ^ 2

def wNormSq (s : Phase) : ℝ := s 2 ^ 2 + s 3 ^ 2

/-- The totalized real-valued extension of Equation (1.1) of Joung--van Koert.
It agrees with the planar circular restricted three-body Hamiltonian on the
collision-free domain (and the source's physical range `0 ≤ μ ≤ 1`). -/
def jacobiHamiltonian (μ : ℝ) (s : Phase) : ℝ :=
  (s 2 ^ 2 + s 3 ^ 2) / 2 + s 0 * s 3 - s 1 * s 2
    - (1 - μ) / Real.sqrt ((s 0 + μ) ^ 2 + s 1 ^ 2)
    - μ / Real.sqrt ((s 0 - 1 + μ) ^ 2 + s 1 ^ 2)

def collisionFree (μ : ℝ) (s : Phase) : Prop :=
  0 < (s 0 + μ) ^ 2 + s 1 ^ 2 ∧
  0 < (s 0 - 1 + μ) ^ 2 + s 1 ^ 2

def coordinateVector (i : Fin 4) : Phase :=
  fun j => if j = i then 1 else 0

def partialDerivative (F : Phase → ℝ) (s : Phase) (i : Fin 4) : ℝ :=
  fderiv ℝ F s (coordinateVector i)

/-- The canonical Hamiltonian vector field `(∂H/∂p, -∂H/∂q)`. -/
def hamiltonianVectorField (F : Phase → ℝ) (s : Phase) : Phase :=
  ![partialDerivative F s 2, partialDerivative F s 3,
    -partialDerivative F s 0, -partialDerivative F s 1]

def isCriticalPoint (F : Phase → ℝ) (s : Phase) : Prop :=
  DifferentiableAt ℝ F s ∧ fderiv ℝ F s = 0

def criticalValueSet (μ : ℝ) : Set ℝ :=
  {e : ℝ | ∃ s : Phase,
    collisionFree μ s ∧ isCriticalPoint (jacobiHamiltonian μ) s ∧
      jacobiHamiltonian μ s = e}

/-- A collision-free equilibrium whose position lies strictly between the two
primaries on their common axis. -/
def IsInnerLagrangePoint (μ : ℝ) (s : Phase) : Prop :=
  collisionFree μ s ∧ isCriticalPoint (jacobiHamiltonian μ) s ∧
    -μ < s 0 ∧ s 0 < 1 - μ ∧ s 1 = 0

/-- The infimum of the collision-free critical values. For `0 < μ < 1`, the
identification theorem below is intended to show that this is `H(L₁)` in the
source's energy convention. -/
def firstCriticalValue (μ : ℝ) : ℝ :=
  sInf (criticalValueSet μ)

/-- The source writes a Jacobi energy level as `H = -c`; being below the first
critical value therefore means `-c < H(L₁)`. -/
def belowFirstCriticalValue (μ c : ℝ) : Prop :=
  -c < firstCriticalValue μ

/-- Squared distance to the second collision after the complex squaring map. -/
def secondCollisionDistanceSq (s : Phase) : ℝ :=
  (2 * (s 0 ^ 2 - s 1 ^ 2) - 1) ^ 2 + (4 * s 0 * s 1) ^ 2

/-- The totalized real-valued extension of Equation (2.2) of Joung--van Koert;
it agrees with the source formula where `secondCollisionDistanceSq s > 0`. -/
def leviCivitaHamiltonian (μ c : ℝ) (s : Phase) : ℝ :=
  wNormSq s / 2 + c * zNormSq s - (1 - μ) / 2
    + 2 * zNormSq s * (s 0 * s 3 - s 1 * s 2)
    - μ * (s 0 * s 3 + s 1 * s 2)
    - μ * zNormSq s / Real.sqrt (secondCollisionDistanceSq s)

/-- A canonical point over collision with the primary at `q=(-μ,0)`. -/
def leftCollisionPoint (μ : ℝ) : Phase :=
  ![0, 0, Real.sqrt (1 - μ), 0]

/-- The inverse position part of the Levi-Civita coordinate change
`q + μ = 2z²`. -/
def leviCivitaPosition (μ : ℝ) (s : Phase) : Plane :=
  ![2 * (s 0 ^ 2 - s 1 ^ 2) - μ, 4 * s 0 * s 1]

/-- The inverse momentum part of the Levi-Civita coordinate change
`p = w / conj z`, totalized at `z = 0`. -/
def leviCivitaMomentum (s : Phase) : Plane :=
  ![(s 2 * s 0 - s 3 * s 1) / zNormSq s,
    (s 2 * s 1 + s 3 * s 0) / zNormSq s]

/-- The collision-free inverse Levi-Civita coordinate map `(z,w) ↦ (q,p)`. -/
def leviCivitaToJacobi (μ : ℝ) (s : Phase) : Phase :=
  let q := leviCivitaPosition μ s
  let p := leviCivitaMomentum s
  ![q 0, q 1, p 0, p 1]

/-- The rotating-coordinate expression in Joung--van Koert, Proposition 2.2.
Strict positivity is their sufficient pointwise criterion for astronomical
retrograde motion with respect to the primary at `(-μ,0)`. -/
def retrogradeIndicator (μ : ℝ) (s : Phase) : ℝ :=
  let q := leviCivitaPosition μ s
  let p := leviCivitaMomentum s
  (q 0 + μ) * p 1 - q 1 * p 0 - μ * (q 0 + μ)

def regularEnergyLocus (μ c : ℝ) : Set Phase :=
  {s | leviCivitaHamiltonian μ c s = 0 ∧ 0 < secondCollisionDistanceSq s}

/-- The connected component based at the regularized collision over
`q=(-μ,0)`. Its intended physical interpretation uses `0 < μ < 1`. -/
def leftEnergyComponent (μ c : ℝ) : Set Phase :=
  connectedComponentIn (regularEnergyLocus μ c) (leftCollisionPoint μ)

abbrev LeftEnergyState (μ c : ℝ) := {s : Phase // s ∈ leftEnergyComponent μ c}

/-- A continuous flow on the left regularized energy component whose time derivative
is the Hamiltonian vector field of the Levi-Civita Hamiltonian. -/
def IsLeviCivitaHamiltonianFlow (μ c : ℝ)
    (φ : Flow ℝ (LeftEnergyState μ c)) : Prop :=
  ∀ s : LeftEnergyState μ c,
    HasDerivAt (fun t : ℝ => ((φ t s : LeftEnergyState μ c) : Phase))
      (hamiltonianVectorField (leviCivitaHamiltonian μ c) (s : Phase)) 0

/-- Compatibility of a flow with the antipodal deck transformation. This is
the condition needed for the flow to descend from the Levi-Civita cover to its
Moser-regularized quotient. -/
def IsAntipodallyEquivariantFlow (μ c : ℝ)
    (φ : Flow ℝ (LeftEnergyState μ c)) : Prop :=
  ∀ t : ℝ, ∀ s₁ s₂ : LeftEnergyState μ c,
    (s₂ : Phase) = -(s₁ : Phase) →
      ((φ t s₂ : LeftEnergyState μ c) : Phase) =
        -((φ t s₁ : LeftEnergyState μ c) : Phase)

structure PeriodicOrbit {X : Type*} [TopologicalSpace X]
    (φ : Flow ℝ X) where
  point : X
  period : ℝ
  period_pos : 0 < period
  closed : φ period point = point

def orbitSet {μ c : ℝ} {φ : Flow ℝ (LeftEnergyState μ c)}
    (γ : PeriodicOrbit φ) : Set Phase :=
  Set.range (fun t : ℝ => ((φ t γ.point : LeftEnergyState μ c) : Phase))

/-- The recorded period is a least positive period. -/
def IsSimplePeriodicOrbit {X : Type*} [TopologicalSpace X]
    (φ : Flow ℝ X) (γ : PeriodicOrbit φ) : Prop :=
  ∀ t : ℝ, 0 < t → t < γ.period → φ t γ.point ≠ γ.point

/-- The closed Levi-Civita orbit has least positive period and reaches the
antipodal point after half that period. For an antipodally equivariant flow on
a component with free antipodal action, this is the condition that its image
in the antipodal quotient is a prime orbit with a two-fold lifted iterate. -/
def IsAntipodalDoubleCover {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c)) (γ : PeriodicOrbit φ) : Prop :=
  IsSimplePeriodicOrbit φ γ ∧
    ((φ (γ.period / 2) γ.point : LeftEnergyState μ c) : Phase) =
      -(γ.point : Phase)

def relativePosition (μ : ℝ) (s : Phase) : Plane :=
  let q := leviCivitaPosition μ s
  ![q 0 + μ, q 1]

/-- A collision-free plane curve has the specified integer-style winding when
it admits a continuous polar lift whose angle changes by `2π * turns` over the
given period. -/
def HasPolarWinding (curve : ℝ → Plane) (period turns : ℝ) : Prop :=
  ∃ ρ θ : ℝ → ℝ,
    Continuous ρ ∧ Continuous θ ∧
    (∀ t : ℝ, 0 < ρ t) ∧
    (∀ t : ℝ,
      curve t = ![ρ t * Real.cos (θ t), ρ t * Real.sin (θ t)]) ∧
    (∀ t : ℝ, ρ (t + period) = ρ t) ∧
    (∀ t : ℝ, θ (t + period) = θ t + 2 * Real.pi * turns)

def jacobiQ₂Reflection (s : Phase) : Phase :=
  ![s 0, -s 1, -s 2, s 3]

/-- Data that represent a chosen lift of a prime noncontractible quotient
orbit when the component carries a free invariant antipodal cover and the flow
is equivariant. `period` is the intended quotient period: after that time the
chosen lift reaches its antipode, and no earlier positive time reaches either
candidate lift. -/
structure AntipodalPeriodicTrajectory {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c)) where
  point : LeftEnergyState μ c
  period : ℝ
  period_pos : 0 < period
  antipodal_closed :
    ((φ period point : LeftEnergyState μ c) : Phase) = -(point : Phase)
  prime : ∀ t : ℝ, 0 < t → t < period →
    ((φ t point : LeftEnergyState μ c) : Phase) ≠ (point : Phase) ∧
    ((φ t point : LeftEnergyState μ c) : Phase) ≠ -(point : Phase)

def IsQ₂SymmetricAntipodalTrajectory {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (δ : AntipodalPeriodicTrajectory φ) : Prop :=
  ∀ t : ℝ,
    leviCivitaToJacobi μ
        ((φ (-t) δ.point : LeftEnergyState μ c) : Phase) =
      jacobiQ₂Reflection
        (leviCivitaToJacobi μ
          ((φ t δ.point : LeftEnergyState μ c) : Phase))

/-- The geometric retrograde orbit in Birkhoff's shooting sense, represented
by one lifted period of its prime noncontractible quotient trajectory. Its
Jacobi position is a simple collision-free loop of winding `+1` around the
chosen primary and has the shooting construction's `q₂`-reflection symmetry.
The continuous polar lift permits temporary angular reversals, so this is
weaker than Joung--van Koert's pointwise astronomical inequality. -/
def IsGeometricBirkhoffRetrogradeTrajectory {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (δ : AntipodalPeriodicTrajectory φ) : Prop :=
    (∀ t : ℝ,
      0 < zNormSq ((φ t δ.point : LeftEnergyState μ c) : Phase)) ∧
    IsQ₂SymmetricAntipodalTrajectory φ δ ∧
    Set.InjOn
      (fun t : ℝ =>
        relativePosition μ ((φ t δ.point : LeftEnergyState μ c) : Phase))
      (Set.Ico 0 δ.period) ∧
    HasPolarWinding
      (fun t : ℝ =>
        relativePosition μ ((φ t δ.point : LeftEnergyState μ c) : Phase))
      δ.period 1

/-- The closed Levi-Civita double lift of an antipodally closed trajectory. -/
def antipodalTrajectoryDoubleLift {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hanti : IsAntipodallyEquivariantFlow μ c φ)
    (δ : AntipodalPeriodicTrajectory φ) : PeriodicOrbit φ where
  point := δ.point
  period := 2 * δ.period
  period_pos := mul_pos (by norm_num) δ.period_pos
  closed := by
    apply Subtype.ext
    rw [show 2 * δ.period = δ.period + δ.period by ring,
      φ.map_add]
    calc
      ((φ δ.period (φ δ.period δ.point) : LeftEnergyState μ c) : Phase) =
          -((φ δ.period δ.point : LeftEnergyState μ c) : Phase) :=
        hanti δ.period δ.point (φ δ.period δ.point) δ.antipodal_closed
      _ = (δ.point : Phase) := by rw [δ.antipodal_closed]; simp

/-- A periodic orbit satisfying the strict pointwise inequality from
Joung--van Koert, Proposition 2.2. This is a sufficient condition for their
astronomical notion of retrograde motion and is stronger than Birkhoff's
shooting terminology (Remark 2.3). -/
def IsAstronomicallyRetrogradeOrbit {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (γ : PeriodicOrbit φ) : Prop :=
  ∀ t : ℝ,
    0 < zNormSq ((φ t γ.point : LeftEnergyState μ c) : Phase) ∧
    0 < retrogradeIndicator μ ((φ t γ.point : LeftEnergyState μ c) : Phase)

/-- A periodic orbit satisfying the strict pointwise direct-motion inequality
from Joung--van Koert, Proposition 2.2. -/
def IsAstronomicallyDirectOrbit {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (γ : PeriodicOrbit φ) : Prop :=
  ∀ t : ℝ,
    0 < zNormSq ((φ t γ.point : LeftEnergyState μ c) : Phase) ∧
    retrogradeIndicator μ ((φ t γ.point : LeftEnergyState μ c) : Phase) < 0

def planeNormSq (u : Plane) : ℝ := u 0 ^ 2 + u 1 ^ 2

def closedUnitDisk : Set Plane := {u | planeNormSq u ≤ 1}

def openUnitDisk : Set Plane := {u | planeNormSq u < 1}

def unitCircle : Set Plane := {u | planeNormSq u = 1}

/-- The round unit three-sphere in the four real phase coordinates. -/
def unitThreeSphere : Set Phase :=
  {s | zNormSq s + wNormSq s = 1}

/-- A homeomorphism from the selected component to the round three-sphere that
intertwines their antipodal maps. -/
def IsAntipodallyEquivariantSphereHomeomorph {μ c : ℝ}
    (e : LeftEnergyState μ c ≃ₜ {x : Phase // x ∈ unitThreeSphere}) : Prop :=
  ∀ s₁ s₂ : LeftEnergyState μ c,
    (s₂ : Phase) = -(s₁ : Phase) →
      ((e s₂ : {x : Phase // x ∈ unitThreeSphere}) : Phase) =
        -((e s₁ : {x : Phase // x ∈ unitThreeSphere}) : Phase)

/-- A smooth embedded disk whose boundary is a periodic orbit, whose interior is
transverse to the Hamiltonian flow, and which every other trajectory meets at
arbitrarily large positive and negative times. -/
def DiskLikeGlobalSurfaceOfSection {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c)) (γ : PeriodicOrbit φ) : Prop :=
  ∃ page : Plane → Phase,
    (∀ u ∈ closedUnitDisk, ContDiffAt ℝ ∞ page u) ∧
    (∀ u ∈ closedUnitDisk, page u ∈ leftEnergyComponent μ c) ∧
    Set.InjOn page closedUnitDisk ∧
    (∀ u ∈ closedUnitDisk, Function.Injective (fderiv ℝ page u)) ∧
    (∀ u ∈ openUnitDisk,
      hamiltonianVectorField (leviCivitaHamiltonian μ c) (page u) ∉
        Set.range (fderiv ℝ page u)) ∧
    page '' unitCircle = orbitSet γ ∧
    (∀ s : LeftEnergyState μ c, (s : Phase) ∉ orbitSet γ →
      (∀ R : ℝ, ∃ t : ℝ, R < t ∧
        ((φ t s : LeftEnergyState μ c) : Phase) ∈ page '' openUnitDisk) ∧
      (∀ R : ℝ, ∃ t : ℝ, t < R ∧
        ((φ t s : LeftEnergyState μ c) : Phase) ∈ page '' openUnitDisk))

/-- The relation that identifies equal or antipodal states of the selected
Levi-Civita component. In the physical subcritical regime, this is the deck
relation for the cover in Joung--van Koert, Proposition 2.4. -/
def antipodalEquivalent {μ c : ℝ}
    (x y : LeftEnergyState μ c) : Prop :=
  (x : Phase) = (y : Phase) ∨ (x : Phase) = -(y : Phase)

/-- The selected component is preserved by the antipodal deck map. -/
def IsAntipodallyInvariantComponent (μ c : ℝ) : Prop :=
  ∀ s : Phase,
    s ∈ leftEnergyComponent μ c ↔ -s ∈ leftEnergyComponent μ c

/-- The antipodal deck map has no fixed point on the selected component. -/
def IsAntipodallyFreeComponent (μ c : ℝ) : Prop :=
  ∀ s : LeftEnergyState μ c, (s : Phase) ≠ -(s : Phase)

/-- The equivalence relation generated by the antipodal deck transformation. -/
def antipodalSetoid (μ c : ℝ) : Setoid (LeftEnergyState μ c) where
  r := antipodalEquivalent
  iseqv := by
    constructor
    · intro x
      exact Or.inl rfl
    · intro x y h
      rcases h with h | h
      · exact Or.inl h.symm
      · exact Or.inr (by
          simpa using (congrArg (fun s : Phase => -s) h).symm)
    · intro x y z hxy hyz
      rcases hxy with hxy | hxy <;> rcases hyz with hyz | hyz
      · exact Or.inl (hxy.trans hyz)
      · exact Or.inr (hxy.trans hyz)
      · exact Or.inr (hxy.trans (congrArg (fun s : Phase => -s) hyz))
      · exact Or.inl (hxy.trans (by
          simpa using congrArg (fun s : Phase => -s) hyz))

/-- The selected regularized component modulo the antipodal deck map. Proposition
2.4 of Joung--van Koert identifies this quotient with the relevant Moser
regularized `ℝP³` component in the physical subcritical regime. -/
abbrev AntipodalQuotientState (μ c : ℝ) :=
  Quotient (antipodalSetoid μ c)

def toAntipodalQuotient {μ c : ℝ}
    (s : LeftEnergyState μ c) : AntipodalQuotientState μ c :=
  Quotient.mk (antipodalSetoid μ c) s

/-- The time-`t` map descended to the antipodal quotient. The equivariance
hypothesis makes the result independent of the chosen lift. -/
def quotientTimeMap {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hanti : IsAntipodallyEquivariantFlow μ c φ) (t : ℝ) :
    AntipodalQuotientState μ c → AntipodalQuotientState μ c :=
  Quotient.map (fun s => φ t s) (by
    intro x y hxy
    rcases hxy with hxy | hxy
    · have h : x = y := Subtype.ext hxy
      subst y
      exact Or.inl rfl
    · exact Or.inr (hanti t y x hxy))

/-- The descended time maps are jointly continuous and satisfy the identity
and composition laws of a real flow. -/
def IsContinuousQuotientDynamics {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hanti : IsAntipodallyEquivariantFlow μ c φ) : Prop :=
  Continuous (Function.uncurry (quotientTimeMap φ hanti)) ∧
  (∀ x : AntipodalQuotientState μ c,
    quotientTimeMap φ hanti 0 x = x) ∧
  ∀ t₁ t₂ : ℝ, ∀ x : AntipodalQuotientState μ c,
    quotientTimeMap φ hanti (t₁ + t₂) x =
      quotientTimeMap φ hanti t₁ (quotientTimeMap φ hanti t₂ x)

def quotientOrbitSet {μ c : ℝ}
    {φ : Flow ℝ (LeftEnergyState μ c)}
    (hanti : IsAntipodallyEquivariantFlow μ c φ)
    (γ : PeriodicOrbit φ) : Set (AntipodalQuotientState μ c) :=
  Set.range (fun t : ℝ =>
    quotientTimeMap φ hanti t (toAntipodalQuotient γ.point))

/-- The half-period image of the lifted orbit is a prime periodic orbit in the
antipodal quotient. -/
def IsPrimeQuotientBinding {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hanti : IsAntipodallyEquivariantFlow μ c φ)
    (γ : PeriodicOrbit φ) : Prop :=
  quotientTimeMap φ hanti (γ.period / 2)
      (toAntipodalQuotient γ.point) = toAntipodalQuotient γ.point ∧
    ∀ t : ℝ, 0 < t → t < γ.period / 2 →
      quotientTimeMap φ hanti t (toAntipodalQuotient γ.point) ≠
        toAntipodalQuotient γ.point

abbrev ClosedDiskPoint := {u : Plane // u ∈ closedUnitDisk}

def closedDiskInterior : Set ClosedDiskPoint :=
  {u | (u : Plane) ∈ openUnitDisk}

def closedDiskBoundary : Set ClosedDiskPoint :=
  {u | (u : Plane) ∈ unitCircle}

abbrev ClosedDiskInteriorPoint :=
  {u : ClosedDiskPoint // u ∈ closedDiskInterior}

/-- The quotient page induced by a chosen smooth lift on the closed disk. -/
def quotientDiskPage {μ c : ℝ} (page : Plane → Phase)
    (hpage : ∀ u ∈ closedUnitDisk, page u ∈ leftEnergyComponent μ c) :
    ClosedDiskPoint → AntipodalQuotientState μ c :=
  fun u => toAntipodalQuotient
    ⟨page (u : Plane), hpage (u : Plane) u.property⟩

def quotientDiskInteriorPage {μ c : ℝ} (page : Plane → Phase)
    (hpage : ∀ u ∈ closedUnitDisk, page u ∈ leftEnergyComponent μ c) :
    ClosedDiskInteriorPoint → AntipodalQuotientState μ c :=
  fun u => quotientDiskPage page hpage u.1

/-- A cover-lift encoding of a rational two-disk global surface of section in
the topological antipodal quotient. The lifted disk is smooth
and immersive, its quotient interior is embedded and disjoint from the binding,
and antipodal boundary parameters are exactly the fibers of the two-fold
boundary map. Transversality is checked on the lift. Arbitrarily far positive
and negative returns are stated for the well-defined descended time maps. -/
def RationalDiskLikeGlobalSurfaceOfSection {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hanti : IsAntipodallyEquivariantFlow μ c φ)
    (γ : PeriodicOrbit φ) : Prop :=
  IsAntipodallyInvariantComponent μ c ∧
  IsAntipodallyFreeComponent μ c ∧
  IsContinuousQuotientDynamics φ hanti ∧
  IsPrimeQuotientBinding φ hanti γ ∧
  ∃ (page : Plane → Phase)
      (hpage : ∀ u ∈ closedUnitDisk,
        page u ∈ leftEnergyComponent μ c),
    (∀ u ∈ closedUnitDisk, ContDiffAt ℝ ∞ page u) ∧
    Set.InjOn page closedUnitDisk ∧
    (∀ u ∈ closedUnitDisk, Function.Injective (fderiv ℝ page u)) ∧
    (∀ u ∈ openUnitDisk,
      hamiltonianVectorField (leviCivitaHamiltonian μ c) (page u) ∉
        Set.range (fderiv ℝ page u)) ∧
    page '' unitCircle = orbitSet γ ∧
    Continuous (quotientDiskPage page hpage) ∧
    Topology.IsEmbedding (quotientDiskInteriorPage page hpage) ∧
    (∀ u v : ClosedDiskPoint,
      (quotientDiskPage page hpage u = quotientDiskPage page hpage v ↔
        (u : Plane) = (v : Plane) ∨
          (u ∈ closedDiskBoundary ∧ v ∈ closedDiskBoundary ∧
            (v : Plane) = -(u : Plane)))) ∧
    quotientDiskPage page hpage '' closedDiskBoundary =
      quotientOrbitSet hanti γ ∧
    (∀ x : AntipodalQuotientState μ c,
      x ∉ quotientOrbitSet hanti γ →
      (∀ R : ℝ, ∃ t : ℝ, R < t ∧
        quotientTimeMap φ hanti t x ∈
          quotientDiskPage page hpage '' closedDiskInterior) ∧
      (∀ R : ℝ, ∃ t : ℝ, t < R ∧
        quotientTimeMap φ hanti t x ∈
          quotientDiskPage page hpage '' closedDiskInterior))

/-- Twice differentiability and positive tangential Hessian on a subset. This is
the differential condition used in the convexity calculation; it does not by
itself assert that the subset bounds a convex body. -/
def HasPositiveTangentialHessianOn (F : Phase → ℝ) (S : Set Phase) : Prop :=
  (∀ s ∈ S, ContDiffAt ℝ 2 F s) ∧
  ∀ s ∈ S, ∀ v : Phase, v ≠ 0 → fderiv ℝ F s v = 0 →
    0 < fderiv ℝ (fun x => fderiv ℝ F x v) s v

end

end BirkhoffGlobalSection

Source

Joung--van Koert, equations (1.1) and (2.2), Definition 2.1, Proposition 2.2, and Proposition 2.4, https://arxiv.org/abs/2407.19159v3; Hryniewicz, Definition 1.1, https://arxiv.org/abs/0812.4076v8; Liu--Salomão, Sections 1.1 and 1.4, https://arxiv.org/abs/2506.17867v2.

Read-back

What the Lean code literally says, in plain math · OpenAI Codex

Literal read-back of Def_BirkhoffGlobalSection.lean

Read-back model: OpenAI Codex. Audited file SHA-256: 5cfb32ece539a44cdd2a855dfa3b7ca01d99333f1778f6e7987c901d6379be10.

Phase

Phase is a reducible abbreviation for the real vector space $\mathrm{Fin}(4)\to\mathbb R$ . Its four coordinates may therefore be read as a function on the four-element index type. The type itself does not distinguish the coordinate interpretation $(q_1,q_2,p_1,p_2)$ from $(z_1,z_2,w_1,w_2)$ .

Plane

Plane is a reducible abbreviation for $\mathrm{Fin}(2)\to\mathbb R$ , with no additional structure or domain restriction beyond the inherited real-vector-space and topological structures.

qNormSq

For every $s\in\mathrm{Phase}$ , qNormSq returns $s_0^2+s_1^2$ .

zNormSq

For every $s\in\mathrm{Phase}$ , zNormSq also returns $s_0^2+s_1^2$ ; it is a distinct name with the same formula as qNormSq.

wNormSq

For every $s\in\mathrm{Phase}$ , wNormSq returns $s_2^2+s_3^2$ .

jacobiHamiltonian

For every real $\mu$ and every phase point $s$ , jacobiHamiltonian returns $(s_2^2+s_3^2)/2+s_0s_3-s_1s_2-(1-\mu)/\sqrt{(s_0+\mu)^2+s_1^2}-\mu/\sqrt{(s_0-1+\mu)^2+s_1^2}$ . There is no hypothesis on $\mu$ or $s$ . Real square root and division are total operations, so this definition has a Lean value even when a displayed denominator is zero; it is not a partial function.

collisionFree

For real $\mu$ and phase point $s$ , collisionFree means the conjunction $(s_0+\mu)^2+s_1^2>0$ and $(s_0-1+\mu)^2+s_1^2>0$ . It restricts only the first two coordinates and imposes no mass interval.

coordinateVector

For $i\in\mathrm{Fin}(4)$ , coordinateVector $i$ is the phase vector whose $j$ th coordinate is $1$ when $j=i$ and $0$ otherwise.

partialDerivative

For every function $F:\mathrm{Phase}\to\mathbb R$ , point $s$ , and coordinate $i$ , partialDerivative applies the Fréchet derivative of $F$ at $s$ to coordinateVector $i$ . The operation fderiv is totalized when differentiability fails, so this real number alone does not assert that $F$ is differentiable.

hamiltonianVectorField

For every $F:\mathrm{Phase}\to\mathbb R$ and $s\in\mathrm{Phase}$ , hamiltonianVectorField returns $(D F(s)e_2,D F(s)e_3,-D F(s)e_0,-D F(s)e_1)$ . It is defined through totalized Fréchet derivatives at every point and has its usual derivative interpretation only when the relevant differentiability facts hold.

isCriticalPoint

For every $F:\mathrm{Phase}\to\mathbb R$ and phase point $s$ , isCriticalPoint means that $F$ is Fréchet differentiable at $s$ and its full Fréchet derivative there is the zero continuous linear map.

criticalValueSet

For every real $\mu$ , criticalValueSet is the set of real numbers $e$ for which there exists a phase point $s$ that is collisionFree for $\mu$ , is a differentiable zero-derivative point of jacobiHamiltonian $\mu$ , and satisfies jacobiHamiltonian $\mu\,s=e$ .

IsInnerLagrangePoint

For real $\mu$ and phase point $s$ , IsInnerLagrangePoint means that $s$ is collision-free, jacobiHamiltonian $\mu$ is differentiable at $s$ with zero derivative, $-\mu<s_0<1-\mu$ , and $s_1=0$ . It does not assert uniqueness and contains no restriction on $\mu$ .

firstCriticalValue

For every real $\mu$ , firstCriticalValue is the infimum sInf of criticalValueSet $\mu$ . The definition supplies no nonemptiness, lower-boundedness, or attainment premise, although sInf remains a total Lean term when those properties are unavailable.

belowFirstCriticalValue

For real $\mu,c$ , belowFirstCriticalValue means exactly the strict inequality $-c<\operatorname{sInf}(\mathrm{criticalValueSet}(\mu))$ .

secondCollisionDistanceSq

For phase point $s$ , secondCollisionDistanceSq is $(2(s_0^2-s_1^2)-1)^2+(4s_0s_1)^2$ . It is nonnegative as a sum of squares.

leviCivitaHamiltonian

For arbitrary real $\mu,c$ and phase point $s$ , leviCivitaHamiltonian returns $(s_2^2+s_3^2)/2+c(s_0^2+s_1^2)-(1-\mu)/2+2(s_0^2+s_1^2)(s_0s_3-s_1s_2)-\mu(s_0s_3+s_1s_2)-\mu(s_0^2+s_1^2)/\sqrt{\mathrm{secondCollisionDistanceSq}(s)}$ . It is total at the zero denominator and has no built-in parameter range.

leftCollisionPoint

For every real $\mu$ , leftCollisionPoint is $(0,0,\sqrt{1-\mu},0)$ . If $\mu>1$ , the real square root is $0$ and this point is not on the declared zero-energy locus; no mass hypothesis is part of the definition.

leviCivitaPosition

For real $\mu$ and phase point $s$ , leviCivitaPosition returns the plane point $(2(s_0^2-s_1^2)-\mu,4s_0s_1)$ .

leviCivitaMomentum

For phase point $s$ , leviCivitaMomentum returns $((s_2s_0-s_3s_1)/(s_0^2+s_1^2),(s_2s_1+s_3s_0)/(s_0^2+s_1^2))$ . When $s_0=s_1=0$ , both numerators and the denominator are zero and both coordinates totalize to zero, independently of $(s_2,s_3)$ .

leviCivitaToJacobi

For real $\mu$ and phase point $s$ , leviCivitaToJacobi concatenates leviCivitaPosition $\mu\,s$ and leviCivitaMomentum $s$ into a four-vector. It accepts all phase points and uses the totalized momentum at $z=0$ .

retrogradeIndicator

For real $\mu$ and Levi–Civita phase point $s$ , retrogradeIndicator computes $(q,p)=\mathrm{leviCivitaToJacobi}(\mu,s)$ and returns $(q_1+\mu)p_2-q_2p_1-\mu(q_1+\mu)$ . At $z=0$ it uses the totalized momentum and evaluates to zero.

regularEnergyLocus

For real $\mu,c$ , regularEnergyLocus is the set of phase points satisfying leviCivitaHamiltonian $\mu\,c\,s=0$ and secondCollisionDistanceSq $s>0$ . It excludes the second collision but permits $z=0$ ; the definition does not assert that zero is a regular value.

leftEnergyComponent

For real $\mu,c$ , leftEnergyComponent is the connected component within regularEnergyLocus based at leftCollisionPoint $\mu$ . No premise says the base point lies in the locus, so this set may be empty for parameters where it does not.

LeftEnergyState

For real $\mu,c$ , LeftEnergyState is the subtype of phase points equipped with a proof of membership in leftEnergyComponent $\mu\,c$ .

IsLeviCivitaHamiltonianFlow

For real $\mu,c$ and a real flow $\varphi$ on LeftEnergyState, this predicate requires, for every state $s$ , that the ambient curve $t\mapsto\varphi_t(s)$ have derivative at $t=0$ equal to the Hamiltonian vector field of leviCivitaHamiltonian $\mu,c$ at the ambient point $s$ . It states no separate all-time derivative formula and is vacuous if the state subtype is empty.

IsAntipodallyEquivariantFlow

For real $\mu,c$ and a real flow $\varphi$ on LeftEnergyState, this predicate says that for every $t\in\mathbb R$ and every two states $s_1,s_2$ , if their ambient phase points satisfy $s_2=-s_1$ , then $\varphi_t(s_2)=-\varphi_t(s_1)$ in ambient coordinates. It does not assert that the antipode of every state belongs to the component; absent such pairs, the relevant implications are vacuous.

PeriodicOrbit

For an arbitrary type $X$ with a topological-space instance and a real flow $\varphi$ on $X$ , a PeriodicOrbit contains a point $x\in X$ , a real number $T>0$ , and an equality $\varphi_T(x)=x$ . It does not require $T$ to be least or $x$ to be nonfixed.

orbitSet

For a periodic orbit in a flow on LeftEnergyState, orbitSet is the set of ambient phase points $\varphi_t(\gamma.\mathrm{point})$ as $t$ ranges over all real numbers. It forgets the recorded period and parametrization multiplicity.

IsSimplePeriodicOrbit

For an arbitrary topological type $X$ , real flow $\varphi$ , and PeriodicOrbit $\gamma$ with recorded period $T$ , this predicate requires $\varphi_t(\gamma.\mathrm{point})\ne\gamma.\mathrm{point}$ for every real $t$ with $0<t<T$ . Together with the PeriodicOrbit return at $T$ , this makes $T$ the least positive return time of that point.

IsAntipodalDoubleCover

For a flow on LeftEnergyState and PeriodicOrbit $\gamma$ with period $T$ , this means that $\gamma$ is simple in the preceding sense and the ambient phase point at time $T/2$ equals the negative of its initial point. It does not itself assume component invariance, freeness, flow equivariance, or construct a quotient orbit.

relativePosition

For real $\mu$ and phase point $s$ , relativePosition adds $\mu$ to the first leviCivitaPosition coordinate and leaves the second unchanged, so it simplifies to $(2(s_0^2-s_1^2),4s_0s_1)$ .

HasPolarWinding

For a curve $g:\mathbb R\to\mathrm{Plane}$ and real numbers $P,n$ , HasPolarWinding means that there exist continuous functions $\rho,\theta:\mathbb R\to\mathbb R$ such that $\rho(t)>0$ , $g(t)=(\rho(t)\cos\theta(t),\rho(t)\sin\theta(t))$ , $\rho(t+P)=\rho(t)$ , and $\theta(t+P)=\theta(t)+2\pi n$ for every real $t$ . Neither $P>0$ nor integrality of $n$ is required by this general definition; positivity of $\rho$ forces the curve to avoid the origin, and continuity alone permits angular reversal.

jacobiQ₂Reflection

For a phase point interpreted as $(q_1,q_2,p_1,p_2)$ , jacobiQ₂Reflection returns $(q_1,-q_2,-p_1,p_2)$ .

AntipodalPeriodicTrajectory

For a real flow $\varphi$ on LeftEnergyState, an AntipodalPeriodicTrajectory contains a state $x$ , a real number $P>0$ , an ambient equality $\varphi_P(x)=-x$ , and, for every $0<t<P$ , the conjunction $\varphi_t(x)\ne x$ and $\varphi_t(x)\ne-x$ . It is not itself a PeriodicOrbit because its endpoint is only required to be antipodal. No freeness or equivariance hypothesis is a field, so a self-antipodal point is not excluded by the structure alone.

IsQ₂SymmetricAntipodalTrajectory

For a flow and AntipodalPeriodicTrajectory $\delta$ , this predicate requires, for every real $t$ , that the Jacobi projection of $\varphi_{-t}(\delta.\mathrm{point})$ equal jacobiQ₂Reflection of the projection of $\varphi_t(\delta.\mathrm{point})$ . At $t=0$ it forces the projected coordinates $q_2$ and $p_1$ to be zero.

IsGeometricBirkhoffRetrogradeTrajectory

For a flow and AntipodalPeriodicTrajectory $\delta$ of period $P$ , this predicate requires $zNormSq(\varphi_t\delta.\mathrm{point})>0$ for every real $t$ , the preceding all-time reflection symmetry, injectivity of the chosen-primary relative-position curve on the half-open interval $[0,P)$ , and HasPolarWinding for that curve with period $P$ and turns $1$ . It asserts no winding about the other primary, no sign condition on retrogradeIndicator, and no separate initial $p_2$ inequality.

antipodalTrajectoryDoubleLift

Given a flow $\varphi$ , a proof that it is antipodally equivariant, and an AntipodalPeriodicTrajectory $\delta$ with period $P$ , this definition constructs a PeriodicOrbit with the same point and recorded period $2P$ . Positivity follows from $P>0$ , and closure at $2P$ is proved using the flow composition law, equivariance, and $\varphi_P(x)=-x$ . The constructed record does not by definition include least-period simplicity.

IsAstronomicallyRetrogradeOrbit

For a PeriodicOrbit in a flow on LeftEnergyState, this predicate requires, for every real time $t$ , both $zNormSq(\varphi_t\gamma.\mathrm{point})>0$ and retrogradeIndicator $\mu(\varphi_t\gamma.\mathrm{point})>0$ . It does not require a least period, antipodal endpoint, reflection symmetry, winding, or page.

IsAstronomicallyDirectOrbit

For a PeriodicOrbit in a flow on LeftEnergyState, this predicate requires, for every real time $t$ , both $zNormSq(\varphi_t\gamma.\mathrm{point})>0$ and retrogradeIndicator $\mu(\varphi_t\gamma.\mathrm{point})<0$ . It has the same omissions as the astronomical-retrograde predicate.

planeNormSq

For $u\in\mathrm{Plane}$ , planeNormSq is $u_0^2+u_1^2$ .

closedUnitDisk

closedUnitDisk is the set of plane points $u$ satisfying $u_0^2+u_1^2\le1$ .

openUnitDisk

openUnitDisk is the set of plane points $u$ satisfying $u_0^2+u_1^2<1$ .

unitCircle

unitCircle is the set of plane points $u$ satisfying $u_0^2+u_1^2=1$ .

unitThreeSphere

unitThreeSphere is the subset of Phase satisfying $s_0^2+s_1^2+s_2^2+s_3^2=1$ .

IsAntipodallyEquivariantSphereHomeomorph

For a homeomorphism $e$ from LeftEnergyState to the subtype unitThreeSphere, this predicate requires that for every existing pair $s_1,s_2$ with ambient $s_2=-s_1$ , the ambient sphere points obey $e(s_2)=-e(s_1)$ . It does not itself assert that the component is closed under antipodes.

DiskLikeGlobalSurfaceOfSection

For a flow $\varphi$ and PeriodicOrbit $\gamma$ , this predicate requires a total map $p:\mathrm{Plane}\to\mathrm{Phase}$ such that: $p$ is $C^\infty$ at every closed-disk point; the closed-disk image lies in leftEnergyComponent; $p$ is injective on the closed disk; $D p(u)$ is injective at every closed-disk point; the Hamiltonian vector field at $p(u)$ is outside the range of $D p(u)$ for every open-disk point; the image of the unit circle equals orbitSet $\gamma$ ; and, for every LeftEnergyState $s$ outside that orbit set, for every real bound $R$ there is a time $t>R$ with $\varphi_t(s)$ on the open page and a time $t<R$ with $\varphi_t(s)$ on the open page. Thus returns are required arbitrarily far in both time directions. No first-return time, local no-return clause, boundary parametrization, or assumption that $\varphi$ is the Hamiltonian flow is included.

antipodalEquivalent

For two LeftEnergyState values $x,y$ , antipodalEquivalent means the disjunction that their ambient phase points are equal or that the ambient point of $x$ is the negative of that of $y$ .

IsAntipodallyInvariantComponent

For real $\mu,c$ , this predicate requires, for every ambient phase point $s$ , that $s$ belongs to leftEnergyComponent $\mu,c$ if and only if $-s$ belongs to it.

IsAntipodallyFreeComponent

For real $\mu,c$ , this predicate requires every state $s$ in LeftEnergyState to satisfy the ambient inequality $s\ne-s$ . It is vacuous on an empty component.

antipodalSetoid

For real $\mu,c$ , antipodalSetoid equips LeftEnergyState with the equivalence relation antipodalEquivalent, namely equality or ambient antipodality. Reflexivity, symmetry, and transitivity are proved in the definition without assuming component invariance or freeness; if an antipodal point is absent from the subtype, no pair involving that absent point is created.

AntipodalQuotientState

For real $\mu,c$ , AntipodalQuotientState is the quotient of LeftEnergyState by antipodalSetoid. It exists whether or not the selected component is invariant or the action is free.

toAntipodalQuotient

For implicit real $\mu,c$ and a LeftEnergyState $s$ , toAntipodalQuotient is the quotient class of $s$ under equality-or-antipodality.

quotientTimeMap

For implicit real $\mu,c$ , a real flow $\varphi$ , a proof $h$ of antipodal equivariance, and time $t$ , quotientTimeMap is the function on AntipodalQuotientState sending the class of $s$ to the class of $\varphi_t(s)$ . Its well-definedness proof uses equality for equal representatives and $h$ for antipodal representatives. Component invariance and freeness are not arguments to this construction.

IsContinuousQuotientDynamics

For a flow $\varphi$ and equivariance proof $h$ , this predicate is the conjunction that the uncurried map $(t,x)\mapsto\mathrm{quotientTimeMap}(t,x)$ is continuous, that time zero fixes every quotient state, and that for every real $t_1,t_2$ and quotient state $x$ , the time- $(t_1+t_2)$ map equals the time- $t_1$ map applied after the time- $t_2$ map. On an empty quotient state, the identity and composition clauses are vacuous, while continuity remains the continuity of the corresponding map with empty state factor.

quotientOrbitSet

For a flow, equivariance proof, and PeriodicOrbit $\gamma$ , quotientOrbitSet is the range over all real $t$ of quotientTimeMap at time $t$ applied to the quotient class of $\gamma.\mathrm{point}$ .

IsPrimeQuotientBinding

For a flow, equivariance proof, and PeriodicOrbit $\gamma$ with recorded period $T$ , this predicate requires the quotient class of $\gamma.\mathrm{point}$ to return at time $T/2$ and not to return at any time $0<t<T/2$ . It concerns return of one quotient point and does not by itself assert an embedded orbit, page, component invariance, freeness, or continuity of quotient dynamics.

ClosedDiskPoint

ClosedDiskPoint is the subtype of Plane consisting of points in closedUnitDisk.

closedDiskInterior

closedDiskInterior is the subset of ClosedDiskPoint whose underlying plane point lies in openUnitDisk.

closedDiskBoundary

closedDiskBoundary is the subset of ClosedDiskPoint whose underlying plane point lies in unitCircle.

ClosedDiskInteriorPoint

ClosedDiskInteriorPoint is the subtype of ClosedDiskPoint consisting of members of closedDiskInterior; an element therefore carries both closed-disk and open-disk membership.

quotientDiskPage

For implicit real $\mu,c$ , a total page $p:\mathrm{Plane}\to\mathrm{Phase}$ , and a proof that $p(u)$ lies in leftEnergyComponent for every closed-disk $u$ , quotientDiskPage maps a ClosedDiskPoint $u$ to the antipodal quotient class of the state represented by $p(u)$ .

quotientDiskInteriorPage

With the same page and membership proof, quotientDiskInteriorPage restricts quotientDiskPage to ClosedDiskInteriorPoint.

RationalDiskLikeGlobalSurfaceOfSection

For a flow $\varphi$ , an antipodal-equivariance proof $h$ , and PeriodicOrbit $\gamma$ , this predicate first requires antipodal invariance and freeness of leftEnergyComponent, joint continuity plus the identity and composition laws for quotientTimeMap, and a prime quotient return for $\gamma$ at half its recorded period. It then requires a total page $p$ and a proof that its closed-disk image lies in leftEnergyComponent. On the closed disk, $p$ must be $C^\infty$ , injective, and have injective derivative; on the open disk, the Hamiltonian vector field must lie outside the derivative range; and the upstairs unit-circle image must equal orbitSet $\gamma$ . The induced quotientDiskPage must be continuous, and its restriction to the open disk must be a topological embedding. For every two closed-disk parameters $u,v$ , their quotient page values must be equal if and only if either $u=v$ , or both are boundary points and $v=-u$ . The quotient image of the disk boundary must equal quotientOrbitSet $\gamma$ . Finally, for every quotient state outside that quotient orbit and every real $R$ , some $t>R$ and some $t<R$ must send the state into the quotient image of the disk interior. The predicate does not construct a smooth structure on the quotient, require quotient-level transversality, specify a first-return map, or identify the quotient with a named manifold.

HasPositiveTangentialHessianOn

For $F:\mathrm{Phase}\to\mathbb R$ and $S\subseteq\mathrm{Phase}$ , this predicate requires $F$ to be $C^2$ at every $s\in S$ and, for every such $s$ and every nonzero phase vector $v$ with $D F(s)v=0$ , requires $D(x\mapsto D F(x)v)(s)v>0$ . The directions are defined by the kernel of $D F(s)$ , not by a separately defined tangent space of $S$ . It does not require $F$ to be constant on $S$ , $D F(s)$ to be nonzero, or $S$ to bound a convex body, and it is vacuous when $S$ is empty.

Human review

Endorsed by Shuze Chen · Sep 12, 2026
Endorsed by Yivy Yu · Sep 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph