Persistence of strict convexity under perturbation
OpenBirkhoffGlobalSection.strict_convex_star_shaped_persistsStrict convexity and star-shapedness persist under small parameter changes. Both are open conditions on the model data, so a reference model with the property outside a fixed set perturbs to a uniform one-sided subcritical strip, with a model at every nearby parameter pair.
This is the perturbation half: it turns the single critical computation into the uniform strip, with no further geometric input.
Retired (2026-09-30). This statement is vacuous: the type RegularizationModel (1/2) 2 is empty. At the critical level the left component contains the saddle-center lift , a zero of the Levi-Civita field, where vectorField and model_regular cannot both hold (see the accepted disproofs of BirkhoffGlobalSection.critical_strict_convex_star_shaped and BirkhoffGlobalSection.critical_reference_model_exists). Its sibling is disproved, so the reduction that introduced it cannot close. No replacement node exists yet; a repaired reduction of BirkhoffGlobalSection.regularization_model_convex_away_from_saddle_center must work at subcritical levels directly.
import Definitions.Def_BirkhoffGlobalSection_RegularizationModel
namespace BirkhoffGlobalSection
theorem strict_convex_star_shaped_persists
(U : Set Phase)
(M₀ : RegularizationModel (1 / 2) 2)
(hM₀ : ∀ s ∈ leftEnergyComponent (1 / 2) 2, s ∉ U →
IsStrictlyConvexStarShapedAt M₀.modelHamiltonian (M₀.toModel s)) :
∃ ε η : ℝ, 0 < ε ∧ 0 < η ∧
∀ μ c : ℝ, 0 < μ → μ < 1 →
|μ - 1 / 2| < ε → c < 2 + η → belowFirstCriticalValue μ c →
∃ M : RegularizationModel μ c,
∀ s ∈ leftEnergyComponent μ c, s ∉ U →
IsStrictlyConvexStarShapedAt M.modelHamiltonian (M.toModel s) := by sorry
end BirkhoffGlobalSection