Proposition 4.4 — narrow-range convexity

Open

BirkhoffRestrictedThreeBody.convex_narrow_range

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let

0\le\mu\le\frac12, \qquad 2.1\le c\le2.1+10^{-6}.

Then the compact component $\Sigma_{\mu,c}$ of the Levi-Civita-regularized energy hypersurface is strictly convex. Concretely, for every $s\in\Sigma_{\mu,c}$ and every nonzero tangent vector $v$ satisfying $dK_{\mu,c}(s)[v]=0$ , the tangential second derivative is positive:

d\bigl(x\mapsto dK_{\mu,c}(x)[v]\bigr)(s)[v]>0.

This is the positive-tangential-Hessian conclusion of Proposition 4.4 used to prove Theorem 1.5. It is a known result in the narrow validated parameter interval and supplies the current convexity frontier toward Birkhoff's conjecture.

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)$ ; every parameter endpoint is included.

Preamble

import Definitions.Def_BirkhoffRestrictedThreeBody

Formal statement

namespace BirkhoffRestrictedThreeBody

/-- Joung--van Koert, Theorem 1.5, expressed as positivity of the tangential Hessian. -/
theorem convex_narrow_range (μ c : ℝ) (hμ0 : 0 ≤ μ) (hμhalf : μ ≤ 1 / 2)
    (hc0 : 21 / 10 ≤ c) (hc1 : c ≤ 21 / 10 + 1 / 1000000) :
    IsStrictlyConvexLevel (leviCivitaHamiltonian μ c) (leftEnergyComponent μ c) := 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. 20, Proposition 4.4 and proof of Theorem 1.5; statement on p. 3, Theorem 1.5.

Read-back

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

For every pair of real numbers $\mu,c$ satisfying the closed endpoint conditions

0\le \mu\le \frac12,\qquad \frac{21}{10}\le c\le \frac{21}{10}+\frac{1}{1{,}000{,}000}

(that is, $0\le\mu\le0.5$ and $2.1\le c\le2.100001$ ), define, for $s=(z_1,z_2,w_1,w_2)\in\mathbb R^4$ ,

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

and

K_{\mu,c}(s)= \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(s)}}.

Let

E_{\mu,c}=\{s\in\mathbb R^4:K_{\mu,c}(s)=0\ \text{and}\ D(s)>0\},

and let $C_{\mu,c}$ be the connected component within $E_{\mu,c}$ containing

a_\mu=(0,0,\sqrt{1-\mu},0).

Then, for every $s\in C_{\mu,c}$ and every vector $v\in\mathbb R^4$ , if $v\ne0$ and the Fréchet derivative of $K_{\mu,c}$ at $s$ , applied to $v$ , is zero,

D K_{\mu,c}(s)[v]=0,

then

D\!\left(x\mapsto D K_{\mu,c}(x)[v]\right)(s)[v]>0.

Thus the asserted positivity concerns exactly the nonzero directions annihilated by the first derivative; it makes no assertion for $v=0$ or for directions with $D K_{\mu,c}(s)[v]\ne0$ , and it concerns only the indicated connected component, not every point of $E_{\mu,c}$ . The strict inequality $D(s)>0$ excludes points where the displayed square-root denominator is zero. Mathlib’s fderiv is a total operation, taking the value zero when the relevant Fréchet derivative does not exist, so the displayed conditions and conclusion are literally statements about that total derivative operation. Under the stated bound on $\mu$ , $a_\mu\in E_{\mu,c}$ : at this point $D(a_\mu)=1$ and $K_{\mu,c}(a_\mu)=0$ ; hence the component quantified over is not empty, including at all four closed interval endpoints for $\mu$ and $c$ .

View graph