Proposition 4.4 — positive tangential Hessian

Proved

BirkhoffGlobalSection.positive_tangential_hessian

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $0\leq\mu\leq1/2$ and $2.1\leq c\leq2.1+10^{-6}$ . The Levi-Civita Hamiltonian is $C^2$ at every point of the selected energy component, and its tangential Hessian is positive definite: for every nonzero $v$ with $dK_{\mu,c}(s)[v]=0$ ,

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

This is the positive-tangential-Hessian clause of Joung--van Koert, Proposition 4.4. The statement deliberately does not use this clause alone as the definition of a convex body. The cited computation uses CAPD 5.3.0 and the batch scripts in the public soir/convexity directory.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- Joung--van Koert, Proposition 4.4: the tangential Hessian is positive
definite throughout the validated parameter interval. -/
theorem positive_tangential_hessian (μ c : ℝ)
    (hμ0 : 0 ≤ μ) (hμhalf : μ ≤ 1 / 2)
    (hc0 : 21 / 10 ≤ c) (hc1 : c ≤ 21 / 10 + 1 / 1000000) :
    HasPositiveTangentialHessianOn
      (leviCivitaHamiltonian μ c) (leftEnergyComponent μ c) := by sorry

end BirkhoffGlobalSection

Source

Joung--van Koert, Proposition 4.4, https://arxiv.org/abs/2407.19159v3. The formal row asserts the positive-tangential-Hessian clause, not the proposition's separate Gauss--Kronecker-curvature conclusion.

Read-back

What the Lean code literally says, in plain math · OpenAI Codex

Read-back model: OpenAI Codex. File SHA-256: f9b5571cc8696e0045a89a4c1399044497f8081d65a5c86bb157404ca02b5fb5. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ,c$ in the closed rectangle $0≤μ≤1/2$ and $2.1≤c≤2.100001$ , let $C$ be the connected component, based at $(0,0,\sqrt{1-μ},0)$ , of the set where the Levi–Civita Hamiltonian $K_{μ,c}$ is zero and secondCollisionDistanceSq is positive. The conclusion says that $K_{μ,c}$ is $C^2$ at every $s∈C$ and that, for every $s∈C$ and every nonzero phase vector $v$ with $D K_{μ,c}(s)v=0$ , one has $D(x↦D K_{μ,c}(x)v)(s)v>0$ . The direction condition is membership in the kernel of the first derivative, not a separately defined tangent space of $C$ . The conclusion does not require $D K_{μ,c}(s)\ne0$ , assert that $C$ is a hypersurface or bounds a convex body, or state positivity in directions outside that kernel; if $C$ is empty, both universal clauses are vacuous.

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