Polar action winding pair bound

Proved

BirkhoffGlobalSection.polar_action_winding_pair_bound

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

dynamical-systemstopology

An angle action with antipodal shift and ordered angular gaps trapped below π has directional normalized increments differing by strictly less than one half.

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.polar_action_winding_pair_bound :
∀ (θ : ℝ × ℝ → ℝ)
    (hshift : ∀ t s, θ (t, s + Real.pi) = θ (t, s) + Real.pi)
    (hgap : ∀ s r, s < r → r - s < Real.pi →
      ∀ t, 0 < θ (t, r) - θ (t, s) ∧ θ (t, r) - θ (t, s) < Real.pi)
    (T s r : ℝ),
    |((θ (T, r) - r) / (2 * Real.pi)) - ((θ (T, s) - s) / (2 * Real.pi))| < 1 / 2 := by sorry

Source

Independent extraction of component 4 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