Foundation Circle Winding Path Displacement Loop Int Mul

The winding number

The winding number is a classical idea in topology. Take a closed loop drawn on a circle, meaning a path that starts and ends at the same point. As the path travels, it wraps around the circle some whole number of times, possibly in the negative direction. That whole number is the winding number. A path that goes around once counterclockwise has winding number 1; one that goes around twice clockwise has winding number -2. The winding number is a topological invariant: if you deform the loop continuously without moving its endpoints, the winding number does not change.

For a circle, the winding number can be computed by lifting the path to the real line. The circle is the quotient of the real line by the relation that identifies points that differ by 2π. A lift of a path on the circle is a path on the real line that projects back down to the original path. The lift is not unique, but any two lifts differ by a constant multiple of 2π. The displacement of a lift, its endpoint value minus its starting value, is therefore well defined up to a multiple of 2π. For a closed loop, the displacement must be an integer multiple of 2π, and that integer is the winding number.

In Recognition Science, the machine-checked library of formal theorems formalizes this exact picture. The declaration pathDisplacement_loop_intMul proves that for any closed loop on the circle, the displacement of its lift is an integer multiple of 2π. This is the theorem that makes the winding number an integer. It is proved by showing that the endpoints of the lift land in the same fiber of the covering map, and then using the fact that points in the same fiber differ by an integer multiple of 2π. The proof is fully formal, with no axioms beyond the standard three, and no unproved assumptions.

What this theorem does not claim is just as important. It does not claim that the winding number is always defined for any path, only for closed loops. It does not claim that the winding number is an integer for paths on other spaces, such as a sphere or a torus. It does not claim that the winding number is the only invariant of a loop on the circle; the homotopy class of the loop is determined by the winding number, but that is a separate theorem. The declaration is a precise, local fact about the circle, and its power comes from being exactly that.

/-- A closed path has displacement equal to an integer number of full turns. -/
theorem pathDisplacement_loop_intMul (γ : C(I, SphereOne)) (hloop : γ 1 = γ 0) :
    ∃ k : ℤ, pathDisplacement γ = (k : ℝ) * (2 * Real.pi) := by
  have hfib : trigCirclePoint (pathLift γ 1) = trigCirclePoint (pathLift γ 0) := by
    have h1 : trigCirclePoint (pathLift γ 1) = γ 1 := congrFun (pathLift_lifts γ) 1
    have h0 : trigCirclePoint (pathLift γ 0) = γ 0 := congrFun (pathLift_lifts γ) 0
    rw [h1, h0, hloop]
  obtain ⟨k, hk⟩ := (trigCirclePoint_eq_iff (pathLift γ 1) (pathLift γ 0)).1 hfib
  refine ⟨k, ?_⟩
  rw [pathDisplacement_self, hk]
  ring

/-- **Homotopy invariance of the displacement.**  If two paths are homotopic
relative to their endpoints, they have the same displacement.  This is the core
mechanism by which the winding invariant kills boundaries: the boundary loop of a
singular `2`-simplex is null-homotopic in the contractible standard simplex, so
its displacement vanishes. -/
theorem pathDisplacement_homotopic {γ δ : C(I, SphereOne)}
    (h : γ.HomotopicRel δ {0, 1}) : pathDisplacement γ = pathDisplacement δ := by
  have hend : γ 0 = δ 0 := homotopicRel_apply_zero h
  have he_γ : γ 0 = trigCirclePoint (pathLiftStart γ) := (pathLiftStart_spec γ).symm
  have he_δ : δ 0 = trigCirclePoint (pathLiftStart γ) := by rw [← hend]; exact he_γ
  have key : isCoveringMap_trig.liftPath γ (pathLiftStart γ) he_γ 1
      = isCoveringMap_trig.liftPath δ (pathLiftStart γ) he_δ 1 :=
    isCoveringMap_trig.liftPath_apply_one_eq_of_homotopicRel h (pathLiftStart γ) he_γ he_δ
  have dγ : pathDisplacement γ
      = isCoveringMap_trig.liftPath γ (pathLiftStart γ) he_γ 1 - pathLiftStart γ := by
    rw [pathDisplacement_eq γ (isCoveringMap_trig.liftPath γ (pathLiftStart γ) he_γ)
        (isCoveringMap_trig.liftPath_lifts γ (pathLiftStart γ) he_γ),
      isCoveringMap_trig.liftPath_zero γ (pathLiftStart γ) he_γ]
  have dδ : pathDisplacement δ
      = isCoveringMap_trig.liftPath δ (pathLiftStart γ) he_δ 1 - pathLiftStart γ := by
    rw [pathDisplacement_eq δ (isCoveringMap_trig.liftPath δ (pathLiftStart γ) he_δ)
        (isCoveringMap_trig.liftPath_lifts δ (pathLiftStart γ) he_δ),
      isCoveringMap_trig.liftPath_zero δ (pathLiftStart γ) he_δ]
  rw [dγ, dδ, key]

What this page does not claim

The theorem does not claim that the winding number is defined for open paths. The theorem does not claim that the winding number is an integer for loops on spaces other than the circle. The theorem does not claim that the winding number is the only invariant of a loop on the circle.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/CircleWinding.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: