Lemma 4.2 — regularized momentum bound

Proved

BirkhoffRestrictedThreeBody.momentum_bound

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $0\le\mu\le\tfrac12$ and $c\ge2.1$ . On the compact component $\Sigma_{\mu,c}$ of the Levi-Civita-regularized energy hypersurface corresponding to the primary at $q=(-\mu,0)$ , every state $(z_1,z_2,w_1,w_2)$ satisfies

\sqrt{w_1^2+w_2^2}\le2.

This a priori momentum estimate is Lemma 4.2 of Joung and van Koert. Together with the position bound, it confines the component to a fixed box used in the paper's validated convexity computation.

Formalization Note. The component is selected inside $K_{\mu,c}^{-1}(0)\cap\{D>0\}$ by the base point $(0,0,\sqrt{1-\mu},0)$ ; all parameter endpoints are included.

Preamble

import Definitions.Def_BirkhoffRestrictedThreeBody

Formal statement

namespace BirkhoffRestrictedThreeBody

/-- Joung--van Koert, Lemma 4.2. -/
theorem momentum_bound (μ c : ℝ) (hμ0 : 0 ≤ μ) (hμhalf : μ ≤ 1 / 2)
    (hc : 21 / 10 ≤ c) (s : Phase) (hs : s ∈ leftEnergyComponent μ c) :
    Real.sqrt (wNormSq s) ≤ 2 := by sorry

end BirkhoffRestrictedThreeBody

Source

Joung--van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, https://arxiv.org/abs/2407.19159, p. 19, Lemma 4.2.

Read-back

What the Lean code literally says, in plain math · gpt-5

For all real parameters $\mu,c$ with $0\le \mu\le \tfrac12$ and $c\ge \tfrac{21}{10}$ , and every four-coordinate real state $s=(s_0,s_1,s_2,s_3)\in\mathbb R^4$ , suppose that $s$ lies in the connected component, within the set $\mathcal R_{\mu,c}$ , containing the base point $b_\mu=(0,0,\sqrt{1-\mu},0)$ , where $\mathcal R_{\mu,c}$ consists exactly of the states $x=(x_0,x_1,x_2,x_3)$ satisfying $K_{\mu,c}(x)=0$ and $D(x)>0$ , with $D(x)=\bigl(2(x_0^2-x_1^2)-1\bigr)^2+(4x_0x_1)^2$ and

K_{\mu,c}(x)=\frac{x_2^2+x_3^2}{2}+c(x_0^2+x_1^2)-\frac{1-\mu}{2}+2(x_0^2+x_1^2)(x_0x_3-x_1x_2)-\mu(x_0x_3+x_1x_2)-\frac{\mu(x_0^2+x_1^2)}{\sqrt{D(x)}}.

Then $\sqrt{s_2^2+s_3^2}\le 2$ . The parameter bounds are inclusive, so $\mu=0$ , $\mu=\tfrac12$ , and $c=\tfrac{21}{10}$ are allowed; the state may equal the base point; and the strict condition $D(x)>0$ on the entire defining locus excludes a zero square-root denominator, while no separate nonzero-coordinate, collision-free, differentiability, flow, or strict-energy hypothesis is imposed.

View graph