Normalized plane family angle unique
ProvedBirkhoffGlobalSection.normalized_plane_family_angle_uniquedynamical-systemstopology
Two jointly continuous positive polar angle lifts of the same plane family, both normalized to s at time zero, are identical.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_winding_interval_bundle open BirkhoffGlobalSection Set Filter Topology open scoped ContDiff Topology set_option maxHeartbeats 800000 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.normalized_plane_family_angle_unique :
∀ (v : ℝ × ℝ → Plane)
(ρ σ θ ψ : ℝ × ℝ → ℝ) (hθ : Continuous θ) (hψ : Continuous ψ)
(hρ : ∀ x, 0 < ρ x) (hσ : ∀ x, 0 < σ x)
(hθ0 : ∀ s, θ (0, s) = s) (hψ0 : ∀ s, ψ (0, s) = s)
(hvθ : ∀ x, v x = ![ρ x * Real.cos (θ x), ρ x * Real.sin (θ x)])
(hvψ : ∀ x, v x = ![σ x * Real.cos (ψ x), σ x * Real.sin (ψ x)]),
θ = ψ := by sorrySource
Independent extraction of component 3 of the Proved theorem BirkhoffGlobalSection.contact_winding_interval_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_winding_interval_bundle.lean. Exact original component retained.