Convex model sphere contact frame reconstruction
ProvedBirkhoffGlobalSection.convex_model_sphere_contact_frame_reconstructionconvex-geometryreal-analysis
Every sphere-contact vector is reconstructed from the convex model sphere contact frame using the displayed pairings.
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_sphere_contact_frame_reconstruction :
∀ {μ c : ℝ}
(M : ConvexRegularizationModel μ c) (u v : Phase) (hu : u ∈ unitThreeSphere)
(hv : u 0 * v 0 + u 1 * v 1 + u 2 * v 2 + u 3 * v 3 = 0)
(hα : phaseRadialContact u v = 0),
let G : Phase → Phase := fun x => (gauge M.body x)⁻¹ • x
let g := TangentialHessian.grad M.modelHamiltonian (G u)
let n := zNormSq g + wNormSq g
let c := transverseFrameCoordinates g (fderiv ℝ G u v)
v = (c 0 / n) • convexModelSphereContactFrame M u 0 +
(c 1 / n) • convexModelSphereContactFrame M u 1 := by sorrySource
Independent extraction of component 6 of the Proved theorem BirkhoffGlobalSection.contact_frame_basis_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_frame_basis_bundle.lean. Exact original component retained.