Lemma 4.2 — Levi-Civita momentum bound

Proved

BirkhoffGlobalSection.momentum_bound

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $0\leq\mu\leq1/2$ and $c\geq2.1$ . Every point $(z,w)$ of the selected Levi-Civita energy component satisfies

|w|\leq2.

This is Joung--van Koert, Lemma 4.2. Together with the position estimate, it confines the component to the compact box used by the validated curvature computation.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- 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 BirkhoffGlobalSection

Source

Joung--van Koert, Lemma 4.2, 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: 3764efa6a996feae0b36a9cf261718188c6de57c406fbb851830fc85005f0f01. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ,c$ and every ambient phase point $s=(z_1,z_2,w_1,w_2)$ , if $0≤μ≤1/2$ , $c≥21/10$ , and $s$ belongs to the connected component of the set where $K_{μ,c}=0$ and secondCollisionDistanceSq is positive based at $(0,0,\sqrt{1-μ},0)$ , then $\sqrt{w_1^2+w_2^2}≤2$ . Both mass endpoints and $c=2.1$ are included, and there is no upper bound on $c$ . No subcriticality premise appears. Because membership is a premise, the universal statement has no instance at parameters for which the selected component is empty.

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