Differentiability of the Jacobi Hamiltonian off collisions

Proved

BirkhoffGlobalSection.jacobi_differentiableAt_of_collisionFree

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

For every real mass parameter $\mu$ and every phase point $s\in\mathbb R^4$ away from both primary collisions, the Jacobi Hamiltonian $H_\mu$ is Fréchet differentiable at $s$ .

\operatorname{collisionFree}(\mu,s)\Longrightarrow H_\mu\text{ is differentiable at }s.

This analytic foundation prevents totalized derivatives at singular points from being mistaken for genuine critical points.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- The Jacobi Hamiltonian is differentiable away from the two collision
positions. -/
theorem jacobi_differentiableAt_of_collisionFree (μ : ℝ) (s : Phase)
    (hs : collisionFree μ s) :
    DifferentiableAt ℝ (jacobiHamiltonian μ) s := by sorry

end BirkhoffGlobalSection

Source

Joung--van Koert, equation (1.1), https://arxiv.org/abs/2407.19159v3. Differentiability off the two displayed collision denominators is the analytic consequence formalized here.

Read-back

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

Read-back model: OpenAI Codex. File SHA-256: 6708242c9e222e9763966f6b1d985741d76870e70d3db01e25764f798c9f01ea. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ$ and phase point $s=(q_1,q_2,p_1,p_2)$ , if $(q_1+μ)^2+q_2^2>0$ and $(q_1-1+μ)^2+q_2^2>0$ , then the total Jacobi function $H_μ(q,p)=(p_1^2+p_2^2)/2+q_1p_2-q_2p_1-(1-μ)/\sqrt{(q_1+μ)^2+q_2^2}-μ/\sqrt{(q_1-1+μ)^2+q_2^2}$ is Fréchet differentiable at $s$ . No mass interval or momentum condition is imposed, and the conclusion is pointwise differentiability rather than a global smoothness statement.

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