Dynamical convexity of a convex regularization model

Open

BirkhoffGlobalSection.convex_model_flow_dynamically_convex

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $M$ be a convex regularization model with model Hamiltonian $H_M$ and convex body $B$ . Then the model Hamiltonian flow on the boundary surface $\partial B$ is dynamically convex: every closed model orbit, including every multiple cover, has transverse winding above one, i.e. Conley--Zehnder index at least $3$ .

\mathrm{IsDynamicallyConvexOn}(H_M, \partial B).

This is the Hofer--Wysocki--Zehnder theorem in the regularization coordinates: the positive tangential Hessian of $H_M$ on $\partial B$ forces the index bound. It supplies the dynamical-convexity input for the rational disk theorem, with no retrograde or binding hypothesis.

Preamble

import Definitions.Def_BirkhoffGlobalSection_DynamicalConvexity
import Definitions.Def_BirkhoffGlobalSection_ConvexRegularizationModel

Formal statement

namespace BirkhoffGlobalSection

theorem convex_model_flow_dynamically_convex {μ c : ℝ}
    (M : ConvexRegularizationModel μ c) :
    IsDynamicallyConvexOn M.modelHamiltonian (frontier M.body) := by sorry

end BirkhoffGlobalSection

Source

Hryniewicz--Salomao, https://arxiv.org/html/1505.02713v3, Corollary 1.8 and Section 4; Liu--Salomao, https://arxiv.org/html/2506.17867v2, Theorem 1.16(ii) (transverse Hopf-fiber clause) and Section 10. Coordinate-level specialization to a centrally symmetric strictly convex model.

View graph