Geometry of the subcritical Levi-Civita component

Proved

BirkhoffGlobalSection.left_energy_component_geometry

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $0<\mu<1$ and $-c<h_1(\mu)$ . Then the selected Levi-Civita component $\Sigma_{\mu,c}$ is compact, $K_{\mu,c}$ is $C^\infty$ there with nonzero derivative at every point, and the antipodal map preserves the component and acts freely. The component admits a homeomorphism to the round unit three-sphere that intertwines the antipodal maps:

e:\Sigma_{\mu,c}\cong S^3, \qquad e(-s)=-e(s).

This is the equivariant sphere model underlying the two-to-one Levi-Civita cover in Joung--van Koert Proposition 2.4. It makes compactness, regularity, topology, and the deck action explicit instead of folding them into the word “component.”

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

open scoped ContDiff

/-- Below the first critical value, the selected Levi-Civita component is a
compact regular hypersurface with an antipodally equivariant sphere model. -/
theorem left_energy_component_geometry (μ c : ℝ)
    (hμ0 : 0 < μ) (hμ1 : μ < 1)
    (hc : belowFirstCriticalValue μ c) :
    IsCompact (leftEnergyComponent μ c) ∧
    (∀ s ∈ leftEnergyComponent μ c,
      ContDiffAt ℝ ∞ (leviCivitaHamiltonian μ c) s ∧
      fderiv ℝ (leviCivitaHamiltonian μ c) s ≠ 0) ∧
    IsAntipodallyInvariantComponent μ c ∧
    IsAntipodallyFreeComponent μ c ∧
    ∃ e : LeftEnergyState μ c ≃ₜ
        {x : Phase // x ∈ unitThreeSphere},
      IsAntipodallyEquivariantSphereHomeomorph e := by sorry

end BirkhoffGlobalSection

Source

Joung--van Koert, Proposition 2.4, https://arxiv.org/abs/2407.19159v3. The row records compactness, regularity, the sphere model, and the free invariant deck action used by the formal quotient.

Read-back

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

Read-back model: OpenAI Codex. File SHA-256: b6e386fd089e2a1b366f9277581d3a136280c02d976f6474b1563d16541963b2. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ,c$ with $0<μ<1$ and $-c<\operatorname{sInf}(V_μ)$ , let $C$ be the connected component, based at $(0,0,\sqrt{1-μ},0)$ , of the set where $K_{μ,c}=0$ and secondCollisionDistanceSq is positive. The conclusion says that $C$ is compact; at every $s∈C$ , $K_{μ,c}$ is $C^∞$ and its Fréchet derivative is nonzero; for every ambient phase point $s$ , $s∈C\iff -s∈C$ ; every state $s∈C$ satisfies $s\ne-s$ ; and there exists a homeomorphism $e$ from the subtype $C$ to the round sphere $S=\{x∈\mathbb R^4:x_0^2+x_1^2+x_2^2+x_3^2=1\}$ such that whenever $s_2=-s_1$ in $C$ , the ambient sphere points obey $e(s_2)=-e(s_1)$ . Here $V_μ$ is the set of collision-free differentiable zero-derivative Jacobi critical values. The conclusion gives a topological homeomorphism rather than a diffeomorphism and does not construct a quotient homeomorphism, orientation, contact structure, or bounding body.

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