Strict convexity at the critical parameters

Disproved

BirkhoffGlobalSection.critical_strict_convex_star_shaped

by caleb · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

celestial-mechanicsdynamical-systemshamiltonian-dynamics

At the critical parameters $\mu=1/2$ , $c=2$ , the elliptic-hyperbolic regularization gives a model whose image is strictly convex and star-shaped at every point outside any fixed open neighborhood $U$ of the saddle-center lifts $(\pm\tfrac12,0,0,0)$ . Outside $U$ the critical surface stays a positive distance from the saddle-centers, where strict convexity holds.

This is the base computation: no parameter perturbation is involved, only the explicit reference model.

Preamble

import Definitions.Def_BirkhoffGlobalSection_RegularizationModel

Formal statement

namespace BirkhoffGlobalSection

theorem critical_strict_convex_star_shaped
    (U : Set Phase) (hU : IsOpen U)
    (hplus : (![1 / 2, 0, 0, 0] : Phase) ∈ U)
    (hminus : (![-(1 / 2), 0, 0, 0] : Phase) ∈ U) :
    ∃ M₀ : RegularizationModel (1 / 2) 2,
      ∀ s ∈ leftEnergyComponent (1 / 2) 2, s ∉ U →
        IsStrictlyConvexStarShapedAt M₀.modelHamiltonian (M₀.toModel s) := by sorry

end BirkhoffGlobalSection

Source

Strict convexity of the equal-mass critical surface in elliptic-hyperbolic regularization (Liu--Salomao, Theorem 1.12, Section 9) and its persistence under small changes of parameters, as used in Section 10: https://arxiv.org/html/2506.17867v2.

View graph