Identification of the first critical value

Proved

BirkhoffGlobalSection.first_critical_value_identification

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $0<\mu<1$ . The set of collision-free critical values of the Jacobi Hamiltonian is nonempty and bounded below. Its infimum is attained at a collision-free equilibrium $L_1$ lying strictly between the primaries on their common axis:

H_\mu(L_1)=h_1(\mu)=\inf\{H_\mu(s):s\text{ is a collision-free critical point}\}.

This makes the phrase “below the first critical value” a proved geometric threshold rather than reliance on the total behavior of sInf.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- The first collision-free critical value is a genuine minimum and is
attained at the equilibrium between the primaries. -/
theorem first_critical_value_identification (μ : ℝ)
    (hμ0 : 0 < μ) (hμ1 : μ < 1) :
    (criticalValueSet μ).Nonempty ∧
    BddBelow (criticalValueSet μ) ∧
    ∃ l₁ : Phase,
      IsInnerLagrangePoint μ l₁ ∧
      jacobiHamiltonian μ l₁ = firstCriticalValue μ := by sorry

end BirkhoffGlobalSection

Source

Liu--Salomão, Section 4 (the five Lagrange values and L1 as the smallest), https://arxiv.org/abs/2506.17867v2; Joung--van Koert, Section 2.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: 6fc25b33fd324b67f368a8f1062fa6ffa6518aab564582976f97b041a147c2da. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ$ with strict $0<μ<1$ , it asserts simultaneously that the set $V_μ$ of Jacobi values attained at collision-free phase points where $H_μ$ is Fréchet differentiable with zero derivative is nonempty and bounded below, and that there exists a phase point $l_1$ which is collision-free, is such a differentiable zero-derivative point, satisfies $-μ<(l_1)_0<1-μ$ and $(l_1)_1=0$ , and has $H_μ(l_1)=\operatorname{sInf}(V_μ)$ . The witness therefore makes the infimum an attained minimum. The endpoints $μ=0,1$ are excluded. No uniqueness of $l_1$ , uniqueness of an inner equilibrium, explicit momentum coordinates, or classification of the other critical values is asserted.

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