Prove2Me

Smoothness of the Levi-Civita Hamiltonian on its regular domain

Proved
BirkhoffGlobalSection.leviCivita_smoothAt_of_secondCollisionFree

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

For every μ,c∈R\mu,c\in\mathbb R, the totalized Levi-Civita Hamiltonian Kμ,cK_{\mu,c} is ambiently C∞C^\infty at every phase point satisfying D(z)>0D(z)>0.

This is exactly the domain on which the remaining inverse-distance denominator in equation (2.2) is nonsingular. It includes the regularized collision over the chosen primary, where z=0z=0 and D(z)=1D(z)=1.

Preamble
import Definitions.Def_BirkhoffGlobalSection
Formal statement
namespace BirkhoffGlobalSection

open scoped ContDiff

/-- The Levi-Civita Hamiltonian is smooth away from the unregularized second
collision. -/
theorem leviCivita_smoothAt_of_secondCollisionFree (μ c : ℝ) (s : Phase)
    (hD : 0 < secondCollisionDistanceSq s) :
    ContDiffAt ℝ ∞ (leviCivitaHamiltonian μ c) s := by sorry

end BirkhoffGlobalSection
Source
Joung--van Koert, equation (2.2), https://arxiv.org/abs/2407.19159v3. Smoothness away from |2z^2-1| = 0 is an analytic consequence of the displayed formula.
Read-back

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

Read-back model: OpenAI Codex. File SHA-256: 045907c97fcd60692d9596cb06db525ec5462336ee3192e24fe6b868178f50ae. This declaration is an admitted by sorry goal, not a proved theorem. For every real μ,cμ,c and phase point s=(z1,z2,w1,w2)s=(z_1,z_2,w_1,w_2), if (2(z12−z22)−1)2+(4z1z2)2>0(2(z_1^2-z_2^2)-1)^2+(4z_1z_2)^2>0, then the full function Kμ,c:R4→RK_{μ,c}:\mathbb R^4→\mathbb R defined by the Levi–Civita Hamiltonian formula is C∞C^∞ at ss. There is no parameter-range or zero-energy assumption, and z=0z=0 is allowed; only the displayed second-collision locus is excluded. At excluded points the totalized function remains defined, but no smoothness is asserted.

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