Foundation Circle Winding Path Lift Endpoint Eq Of Winding Zero

Winding zero and the lift's endpoints

The winding number of a closed curve around a point counts how many times the curve circles that point. A curve that goes around once has winding number 1; a curve that loops twice has 2. A curve that never completes a full circle, or goes out and comes back the same way, has winding number 0. The classical fact is that winding number 0 is exactly the condition under which a loop can be continuously shrunk to a single point without leaving the circle.

In the Recognition Science framework, the circle is represented as the standard unit circle in the plane, and paths on it are continuous maps from the unit interval into that circle. The framework's ledger, a discrete record of events, tracks how far a path's lift travels along the real line. The lift is a way of unrolling the circle into a line, so that a point on the circle corresponds to many possible real numbers, each differing by multiples of 2π. The displacement of a path is the difference between the lift's value at the end and at the start.

The theorem pathLift_endpoint_eq_of_winding_zero states: if a path on the circle has winding number 0, then the lift's value at the endpoint equals its value at the start. In plain language, a path that winds zero times returns to the same point on the unrolled line, not just the same point on the circle. This is the precise statement that a zero-winding loop does not accumulate any net turning.

The proof is short and rests on two earlier results. First, the winding number is defined as the displacement divided by 2π. Second, for any path that starts and ends at the same point on the circle, the displacement is an integer multiple of 2π. If the winding number is 0, then the displacement is 0, so the lift's endpoints coincide. The argument uses only the definitions and basic arithmetic; no additional axioms or unproved assumptions enter.

What the theorem does not claim is that a zero-winding loop is homotopic to a constant path. That stronger statement, that the loop can be continuously deformed to a point, is a separate result in the framework, pathHomotopicRel_const_of_loop_winding_zero, which requires the additional hypothesis that the path is a loop, meaning its start and end points on the circle are equal. The endpoint equality theorem holds for any path with winding zero, even one whose start and end points on the circle differ.

In Recognition Science, this result matters because it makes the winding number a usable invariant. The framework's later computations can choose any convenient lift of a path, knowing that the displacement, and hence the winding number, is independent of that choice. The endpoint equality is the bridge that lets the ledger track turning consistently across all paths.

/-- Zero winding forces the canonical lift endpoints to agree.  This is the
lift-level form consumed by the singular cone construction in
`CircleWindingChain`. -/
theorem pathLift_endpoint_eq_of_winding_zero (γ : C(I, SphereOne))
    (hw : pathWinding γ = 0) :
    pathLift γ 1 = pathLift γ 0 := by
  have hdisp : pathDisplacement γ = 0 := by
    unfold pathWinding at hw
    have hpi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
    rcases (div_eq_zero_iff).mp hw with hzero | hden
    · exact hzero
    · exact False.elim (hpi hden)
  rw [pathDisplacement_self] at hdisp
  linarith

What this page does not claim

The theorem does not claim that a zero-winding path is a loop, nor that it can be shrunk to a point; those require the separate loop hypothesis. The theorem does not claim that the winding number is always an integer for non-loop paths; that is only proved for loops. The theorem does not claim that the lift is unique; it establishes equality of endpoints for the canonical lift, with independence shown by a separate theorem.

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: