The $c \geq 2.1$ range is subcritical

Proved

BirkhoffGlobalSection.numerical_range_subcritical

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $0<\mu\leq1/2$ and $c\geq2.1$ . Then the Jacobi energy $-c$ lies below the first collision-free critical value:

-c<h_1(\mu).

This is an a priori energy half-line containing the positive-mass part of the validated global-section rectangle $2.1\leq c\leq2.1+10^{-6}$ . The endpoint $\mu=0$ belongs to the cited Joung--van Koert theorem but is intentionally outside this first-critical-value row and the formal validated global-section row. The statement connects the positive-mass numerical parameters to the subcritical hypothesis; it does not enlarge the interval on which the computer-assisted global-section theorem is claimed.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- The a priori half-line `c ≥ 2.1` over `0 < μ ≤ 1/2`, which contains the
positive-mass part of Joung--van Koert's validated rectangle, lies below the
first critical Jacobi value. -/
theorem numerical_range_subcritical (μ c : ℝ)
    (hμ0 : 0 < μ) (hμhalf : μ ≤ 1 / 2) (hc : 21 / 10 ≤ c) :
    belowFirstCriticalValue μ c := by sorry

end BirkhoffGlobalSection

Source

Joung--van Koert, Section 4 and Lemma 4.1, https://arxiv.org/abs/2407.19159v3. This row isolates the positive-mass subcritical estimate used for the c >= 2.1 parameter range.

Read-back

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

Read-back model: OpenAI Codex. File SHA-256: 8ee62fd7aca24af0f910d3053d1cb0857d6b21aee366b5c001fc2970874912fc. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ,c$ , if $0<μ≤1/2$ and $21/10≤c$ , then $-c<\operatorname{sInf}(V_μ)$ , where $V_μ$ is the set of all values of the Jacobi Hamiltonian at collision-free phase points where that Hamiltonian is Fréchet differentiable with zero derivative. The endpoint $μ=1/2$ and the endpoint $c=2.1$ are included, $μ=0$ is excluded, and there is no upper bound on $c$ . The conclusion asserts only this strict inequality; it does not assert that $V_μ$ is nonempty or bounded below, that the infimum is attained, or that any regularized component, flow, orbit, or page exists.

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

The c≥2.1c \geq 2.1c≥2.1 range is subcritical

The $c \geq 2.1$ range is subcritical