The selected collision point lies on the energy component

Proved

BirkhoffGlobalSection.leftCollisionPoint_mem_leftEnergyComponent

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $0<\mu<1$ . For every real energy parameter $c$ , the point

(z_1,z_2,w_1,w_2)=(0,0,\sqrt{1-\mu},0)

lies in the selected Levi-Civita component $\Sigma_{\mu,c}$ . At this point $D=1$ and $K_{\mu,c}=0$ , so it is the regularized collision used to anchor the component definition.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- The designated regularized collision point lies on the selected component
for physical mass parameters. -/
theorem leftCollisionPoint_mem_leftEnergyComponent (μ c : ℝ)
    (hμ0 : 0 < μ) (hμ1 : μ < 1) :
    leftCollisionPoint μ ∈ leftEnergyComponent μ c := by sorry

end BirkhoffGlobalSection

Source

Joung--van Koert, equation (2.2), https://arxiv.org/abs/2407.19159v3. Membership of the chosen point follows by direct substitution and anchors the source's selected component.

Read-back

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

Read-back model: OpenAI Codex. File SHA-256: f3a75b1c87895e9858e6f2a075beddee778d6b55c59004aa3ae9b87deaf6522d. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ,c$ with strict $0<μ<1$ , it concludes that $(0,0,\sqrt{1-μ},0)$ belongs to the connected component, based at that same point, of the set where the Levi–Civita Hamiltonian $K_{μ,c}$ equals zero and $(2(z_1^2-z_2^2)-1)^2+(4z_1z_2)^2>0$ . The parameter $c$ is unrestricted and no subcriticality premise appears. The conclusion establishes membership only for the designated point; it does not include its antipode, component invariance, freeness, compactness, or topology.

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