Equation 2.2 — Levi-Civita regularization identity

Proved

BirkhoffGlobalSection.leviCivita_regularization_identity

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $s=(z_1,z_2,w_1,w_2)$ satisfy both $|z|^2>0$ and $D(z)>0$ . Thus neither the regularized collision at the chosen primary nor the remaining singular collision is present. Under the inverse Levi-Civita coordinate change $q+\mu=2z^2$ and $p=w/\bar z$ , the regularized and unregularized Hamiltonians satisfy

K_{\mu,c}(s)=|z|^2\bigl(H_\mu(q,p)+c\bigr).

This is the scalar algebraic identity underlying Joung--van Koert equation (2.2). On $K_{\mu,c}=0$ it identifies the corresponding Jacobi energy as $H_\mu=-c$ ; the vector-field identity and positive time reparametrization are separate dynamical statements.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- Equation (2.2): away from both collision loci, the Levi-Civita Hamiltonian
is the shifted Jacobi Hamiltonian multiplied by `|z|²`. -/
theorem leviCivita_regularization_identity (μ c : ℝ) (s : Phase)
    (hz : 0 < zNormSq s) (hD : 0 < secondCollisionDistanceSq s) :
    leviCivitaHamiltonian μ c s =
      zNormSq s * (jacobiHamiltonian μ (leviCivitaToJacobi μ s) + c) := by sorry

end BirkhoffGlobalSection

Source

Joung--van Koert, equation (2.2) and the immediately following scalar/vector-field relation, 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: 2ca660b2ee0a25bd29b71f88545eb354e5149464a5fb51a707806595497decec. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ,c$ and every phase point $s=(z_1,z_2,w_1,w_2)$ , it assumes $z_1^2+z_2^2>0$ and $(2(z_1^2-z_2^2)-1)^2+(4z_1z_2)^2>0$ , strictly excluding the two displayed collision loci, and concludes $K_{μ,c}(s)=(z_1^2+z_2^2)(H_μ(L_μ(s))+c)$ . Here $L_μ(s)$ has position $(2(z_1^2-z_2^2)-μ,4z_1z_2)$ and momentum $((w_1z_1-w_2z_2)/(z_1^2+z_2^2),(w_1z_2+w_2z_1)/(z_1^2+z_2^2))$ ; $H_μ$ is the declared Jacobi Hamiltonian and $K_{μ,c}$ the declared Levi–Civita Hamiltonian. No parameter range, energy-level conclusion, vector-field relation, orbit correspondence, or time reparametrization 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