Continuous angle increment unique
ProvedBirkhoffGlobalSection.continuous_angle_increment_uniquedynamical-systemstopology
Two continuous real angles with identical sine and cosine at every time have equal increments relative to time zero.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
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.continuous_angle_increment_unique :
∀ (θ ψ : ℝ → ℝ)
(hθ : Continuous θ) (hψ : Continuous ψ)
(hcos : ∀ t, Real.cos (θ t) = Real.cos (ψ t))
(hsin : ∀ t, Real.sin (θ t) = Real.sin (ψ t)),
∀ t, θ t - θ 0 = ψ t - ψ 0 := by sorrySource
Independent extraction of component 3 of the Proved theorem BirkhoffGlobalSection.contact_angular_lift_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_angular_lift_bundle.lean. Exact original component retained.