Convex model gauge differential energy tangent
ProvedBirkhoffGlobalSection.convex_model_gauge_differential_energy_tangentconvex-geometryreal-analysis
At a model boundary point, the gauge differential annihilates every Hamiltonian energy-tangent vector.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained. This is a conditional result for the defined convex regularization model, not a global-section or index-existence theorem.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_frame_basis_bundle open BirkhoffGlobalSection Set Filter SignType open scoped ContDiff Topology set_option linter.unusedVariables false set_option autoImplicit false set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.convex_model_gauge_differential_energy_tangent :
∀ {μ c : ℝ}
(M : ConvexRegularizationModel μ c) (u v : Phase) (hu : u ∈ unitThreeSphere),
let G : Phase → Phase := fun x => (gauge M.body x)⁻¹ • x
fderiv ℝ M.modelHamiltonian (G u) (fderiv ℝ G u v) = 0 := by sorrySource
Independent extraction of component 5 of the Proved theorem BirkhoffGlobalSection.contact_frame_basis_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_frame_basis_bundle.lean. Exact original component retained.