Plane positive polar unique
ProvedBirkhoffGlobalSection.plane_positive_polar_uniquedynamical-systemstopology
Two positive-radius polar representations of the same plane vector have the same radius, cosine and sine.
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.plane_positive_polar_unique :
∀ (v : Plane) (ρ σ θ ψ : ℝ)
(hρ : 0 < ρ) (hσ : 0 < σ)
(hθ : v = ![ρ * Real.cos θ, ρ * Real.sin θ])
(hψ : v = ![σ * Real.cos ψ, σ * Real.sin ψ]),
ρ = σ ∧ Real.cos θ = Real.cos ψ ∧ Real.sin θ = Real.sin ψ := by sorrySource
Independent extraction of component 4 of the Proved theorem BirkhoffGlobalSection.contact_angular_lift_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_angular_lift_bundle.lean. Exact original component retained.