Lemma 4.1 — Levi-Civita position bound

Proved

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

2|z|^2\leq\frac35.

This is the “in particular” conclusion of Joung--van Koert, Lemma 4.1, and confines the regularized position coordinate for the later curvature calculation.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

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

Source

Joung--van Koert, Lemma 4.1, 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: 75b57fe1580b662792ebe66e0d426005ac6f25c2dccf79bb8ab55241e3c1e04f. 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 $2(z_1^2+z_2^2)≤3/5$ . Both mass endpoints and $c=2.1$ are included, and there is no upper bound on $c$ . No subcriticality premise appears. The conclusion is a bound on the Levi–Civita position norm, not on individual coordinates or directly on Jacobi position; if the selected component is empty, no point can satisfy the membership premise.

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