Lemma 4.1 — regularized position bound

Proved

BirkhoffRestrictedThreeBody.position_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

2(z_1^2+z_2^2)\le\frac35.

Equivalently, the regularized position coordinate remains in the disk of squared radius $3/10$ . This a priori estimate is the “in particular” conclusion of Lemma 4.1 and is used to confine the component before checking its curvature.

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

/-- The `2|z|² ≤ 3/5` consequence of Joung--van Koert, Lemma 4.1. -/
theorem position_bound (μ c : ℝ) (hμ0 : 0 ≤ μ) (hμhalf : μ ≤ 1 / 2)
    (hc : 21 / 10 ≤ c) (s : Phase) (hs : s ∈ leftEnergyComponent μ c) :
    2 * zNormSq s ≤ 3 / 5 := 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.1 (in particular clause).

Read-back

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

For every pair of real numbers $\mu,c$ satisfying $0\le \mu\le \tfrac12$ and $c\ge \tfrac{21}{10}$ , and every point $s=(z_1,z_2,w_1,w_2)\in\mathbb R^4$ lying in the connected component, within the set $L_{\mu,c}$ , that contains $\ell_\mu=(0,0,\sqrt{1-\mu},0)$ , where $L_{\mu,c}$ consists exactly of the points $x=(z_1,z_2,w_1,w_2)$ such that $K_{\mu,c}(x)=0$ and $D(x)>0$ , with

D(x)=\bigl(2(z_1^2-z_2^2)-1\bigr)^2+(4z_1z_2)^2

and

K_{\mu,c}(x)=\frac{w_1^2+w_2^2}{2}+c(z_1^2+z_2^2)-\frac{1-\mu}{2}+2(z_1^2+z_2^2)(z_1w_2-z_2w_1)-\mu(z_1w_2+z_2w_1)-\frac{\mu(z_1^2+z_2^2)}{\sqrt{D(x)}},

one has the non-strict bound $2(z_1^2+z_2^2)\le \tfrac35$ . The endpoint cases $\mu=0$ , $\mu=\tfrac12$ , and $c=\tfrac{21}{10}$ are included; $D(x)>0$ ensures that the displayed square-root denominator is positive on $L_{\mu,c}$ , and the hypotheses on $\mu$ ensure that $\ell_\mu\in L_{\mu,c}$ , so the specified component is nonempty. No collision-free condition, flow, periodic-orbit, convexity, or separate restriction on $w_1,w_2$ is assumed beyond membership in that component.

View graph