A loop missing a ray from the origin has winding number zero

Proved

FiniteEnergyPlane.hasLoopWind_zero_of_forall_ne_ray

by Mazecto · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysissymplectic-geometrytopologywinding-numbers

Let $q:\mathbb{R}\to\mathbb{C}$ be continuous and $1$ -periodic, and let $w\in\mathbb{C}\setminus\{0\}$ . If $q(t)\neq s\,w$ for every $t\in\mathbb{R}$ and every real $s\ge 0$ (so $q$ avoids the closed ray from $0$ through $w$ , including $0$ ), then $q$ has winding number $0$ .

A criterion for vanishing winding, for comparing windings of loops in $\mathbb{C}\setminus\{0\}$ .

Formalization Note The conclusion is HasLoopWind q 0 from FiniteEnergyPlane_Winding; the hypothesis is ∀ t, ∀ s : ℝ, 0 ≤ s → q t ≠ s * w with hw : w ≠ 0.

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

/-- A continuous `1`-periodic loop in `ℂ` that misses a closed ray `{s w : s ≥ 0}` (`w ≠ 0`)
has winding number `0`. -/
theorem hasLoopWind_zero_of_forall_ne_ray (q : ℝ → ℂ) (hq : Continuous q)
    (hper : Function.Periodic q 1) (w : ℂ) (hw : w ≠ 0)
    (h : ∀ t, ∀ s : ℝ, 0 ≤ s → q t ≠ s * w) : HasLoopWind q 0 := by
  sorry

end FiniteEnergyPlane

Source

C. Wendl, Lectures on Symplectic Field Theory (2026 notes), arXiv:1612.01009, Section 3.7 (winding numbers of loops in C minus 0); standard.

View graph