Prove2Me

Antipodal symmetry of the Levi-Civita component

Proved
BirkhoffGlobalSection.antipodal_symmetry

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let 0<μ<10<\mu<1 and −c<h1(μ)-c<h_1(\mu). The totalized Levi-Civita formula is even, and on the selected subcritical component the antipodal map is invariant and free:

Kμ,c(−s)=Kμ,c(s),−s∈Σμ,c  ⟺  s∈Σμ,c,s≠−s(s∈Σμ,c).K_{\mu,c}(-s)=K_{\mu,c}(s), \qquad -s\in\Sigma_{\mu,c}\iff s\in\Sigma_{\mu,c}, \qquad s\neq -s\quad(s\in\Sigma_{\mu,c}).

The Hamiltonian equality is an algebraic consequence of the displayed formula, including Lean's totalized extension at the excluded singular locus. Invariance and freeness are the deck-action properties on the physical subcritical component used in Joung--van Koert Proposition 2.4; equation (2.4) names the involution.

Preamble
import Definitions.Def_BirkhoffGlobalSection
Formal statement
namespace BirkhoffGlobalSection

/-- Algebraic evenness of the totalized Levi-Civita formula, together with the
free component-preserving antipodal deck action in the physical subcritical
regime of Joung--van Koert, Proposition 2.4. -/
theorem antipodal_symmetry (μ c : ℝ)
    (hμ0 : 0 < μ) (hμ1 : μ < 1) (hc : belowFirstCriticalValue μ c) :
    (∀ s : Phase,
      leviCivitaHamiltonian μ c (-s) = leviCivitaHamiltonian μ c s) ∧
    IsAntipodallyInvariantComponent μ c ∧
    IsAntipodallyFreeComponent μ c := by sorry

end BirkhoffGlobalSection
Source
Joung--van Koert, equation (2.4) and Proposition 2.4, https://arxiv.org/abs/2407.19159v3.
Read-back

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

Read-back model: OpenAI Codex. File SHA-256: b1ec43e4d2b6dca24511ca4ecd421bdf817cef165b0859c7bc22fd955f08819d. This declaration is an admitted by sorry goal, not a proved theorem. For every real μ,cμ,c with 0<μ<10<μ<1 and −c<sInf⁡(Vμ)-c<\operatorname{sInf}(V_μ), it concludes three facts: for every ambient phase point ss, including points where the Levi–Civita formula uses totalized division, Kμ,c(−s)=Kμ,c(s)K_{μ,c}(-s)=K_{μ,c}(s); for every ambient ss, membership in the selected connected component CC of Kμ,c=0K_{μ,c}=0 with positive second-collision distance satisfies s∈C  ⟺  −s∈Cs∈C\iff -s∈C; and every subtype state s∈Cs∈C satisfies s≠−ss\ne-s. Here CC is based at (0,0,1−μ,0)(0,0,\sqrt{1-μ},0) and VμV_μ is the set of collision-free differentiable zero-derivative Jacobi critical values. The declaration does not mention a flow, so it asserts no flow equivariance or quotient dynamics, and it gives no sphere or quotient-space identification.

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