Linear action antipodal angle

Proved

BirkhoffGlobalSection.linear_action_antipodal_angle

by Mazecto · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemstopology

For a real-linear plane action with normalized continuous positive polar data, adding π to the initial angle adds exactly π to the lifted angle at every time.

All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.

Preamble

import Theorems.Thm_BirkhoffGlobalSection_contact_winding_width_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.linear_action_antipodal_angle :
∀ (A : ℝ → Plane → Plane)
    (ρ θ : ℝ × ℝ → ℝ) (hθ : Continuous θ) (hρ : ∀ x, 0 < ρ x)
    (hθ0 : ∀ s, θ (0, s) = s)
    (hpolar : ∀ t s, A t ![Real.cos s, Real.sin s] =
      ![ρ (t, s) * Real.cos (θ (t, s)), ρ (t, s) * Real.sin (θ (t, s))])
    (hneg : ∀ t p, A t (-p) = -(A t p)),
    ∀ t s, θ (t, s + Real.pi) = θ (t, s) + Real.pi := by sorry

Source

Independent extraction of component 3 of the Proved theorem BirkhoffGlobalSection.contact_winding_width_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_winding_width_bundle.lean. Exact original component retained.

View graph