Convex model contact variation increment unique
ProvedBirkhoffGlobalSection.convex_model_contact_variation_increment_uniqueconvex-geometryreal-analysis
Any two supplied continuous positive-radius polar lifts of the same convex model contact-coordinate trajectory have equal angular increments.
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_angular_lift_bundle open BirkhoffGlobalSection Set Filter Topology open scoped ContDiff Topology set_option linter.unusedVariables false set_option autoImplicit false set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.convex_model_contact_variation_increment_unique :
∀ {μ c : ℝ}
(M : ConvexRegularizationModel μ c) (q : ℝ → Phase)
(Z : ℝ → (Phase →L[ℝ] Phase)) (p : Plane) (ρ σ θ ψ : ℝ → ℝ)
(hθ : Continuous θ) (hψ : Continuous ψ)
(hρ : ∀ t, 0 < ρ t) (hσ : ∀ t, 0 < σ t)
(hvθ : ∀ t, convexModelContactVariationPath M q Z t p =
![ρ t * Real.cos (θ t), ρ t * Real.sin (θ t)])
(hvψ : ∀ t, convexModelContactVariationPath M q Z t p =
![σ t * Real.cos (ψ t), σ t * Real.sin (ψ t)]),
∀ t, θ t - θ 0 = ψ t - ψ 0 := by sorrySource
Independent extraction of component 7 of the Proved theorem BirkhoffGlobalSection.contact_angular_lift_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_angular_lift_bundle.lean. Exact original component retained.