Radial transversality on the critical estimate region

Disproved

BirkhoffGlobalSection.critical_estimate_radial_pos

by Sneed · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Radial transversality on the critical estimate region.

For every point $y$ of the first-quadrant estimate region $\\mathcal{H}_1$ at $\\mu=1/2$ , $h=-2$ , the critical Hamiltonian is transversely star-shaped at $y$ :

d\\hat{H}(y)[y]>0.

Together with tangential Hessian positivity this yields strict convexity star-shaped at $y$ ; it is the transversality half used in Sections 9.3--9.4.

Formalization Note The derivative is the Mathlib Fr\u00e9chet derivative fderiv \\mathbb{R} applied to the radial vector $y$ .

Preamble

import Definitions.Def_BirkhoffGlobalSection_RegularizationModel
import Definitions.Def_BirkhoffGlobalSection_EHCriticalConvexity

Formal statement

namespace BirkhoffGlobalSection

theorem critical_estimate_radial_pos
    (y : Phase) (hy : y ∈ ehEstimateRegion) :
    0 < fderiv ℝ ehCriticalHamiltonian y y := by sorry

end BirkhoffGlobalSection

Source

Liu--Salomao, Finite energy foliations and global dynamics in the restricted three-body problem, https://arxiv.org/html/2506.17867v2, Section 9.2 (elliptic-hyperbolic regularization, mu = 1/2, h = -2), Section 9.3 (Theorems 9.1 and 9.4, eq. 9.11), and Theorem 1.12 as used in Section 10.

View graph