Foundation Circle Lifting

The circle's unwinding

The circle is the simplest shape with a hole, and its one defining feature is that a path around it can wind. A point moving once around returns to its start, but the journey has a quality the return does not record: it went around once, not zero times. To capture that quality, mathematics unwinds the circle into the real line, where each turn becomes a shift by the circumference. The map from the line to the circle, sending a real number to the point at that angle, is the covering map, and the act of lifting a path on the circle up to the line is circle lifting.

The standard fact, known since the nineteenth century, is that this unwinding is complete: any path on the circle lifts uniquely once you choose a starting height on the line, and the endpoint of the lifted path records the net winding. The subtlety is that the lift must agree with itself when the path is deformed, so that a winding number is a property of the loop, not of a particular way of drawing it. The classical tool for this is the path-lifting property of covering spaces, which guarantees that nearby paths lift to nearby paths and that homotopic paths lift to homotopic paths.

In Recognition Science, the framework's machine-checked library of formal theorems establishes the two ingredients this lifting needs. First, the standard simplex, the topological shape used to build singular chains, is contractible and therefore simply connected; this is the hypothesis that makes the path-lifting monodromy invariance work, so that the winding number kills boundaries. Second, the fiber of the covering is described exactly: two real parameters hit the same point on the circle if and only if they differ by an integer multiple of 2π. This deck-transformation description is the algebraic heart of both the well-definedness of the winding number and the value that the fundamental loop winds once.

The contribution of the formal development is to package these facts for the circle as a topological space, not as a special-case construction. It registers the contractibility instance once, states the simple-connectedness theorem explicitly for discoverability, and repackages the covering map as an IsCoveringMap term for direct use with the path-lifting API. No axioms, sorry, or project-local S¹ replacements are used; the results are derived from the standard library's covering space theory.

What this changes is that the winding number, a tool that appears throughout topology and analysis, is now available in the framework with its foundational prerequisites settled. A later module can define the winding number on singular 1-chains of the circle and prove it kills boundaries, knowing the lifting machinery is in place. The circle's unwinding is not an assumption; it is a proved fact.

/-- The topological standard `n`-simplex (the realization domain of a singular
`(n-1)`-simplex) is contractible: it is a nonempty convex set. -/
instance stdSimplex_contractibleSpace (n : ℕ) [NeZero n] :
    ContractibleSpace (stdSimplex ℝ (Fin n)) :=
  (convex_stdSimplex ℝ (Fin n)).contractibleSpace
    ⟨_, single_mem_stdSimplex ℝ (0 : Fin n)⟩

/-- Consequently the standard simplex is simply connected; this is the precise
hypothesis consumed by the path-lifting monodromy invariance used to show the
winding number kills boundaries.  (Stated explicitly for discoverability; it is
also available by instance resolution.) -/
theorem stdSimplex_simplyConnectedSpace (n : ℕ) [NeZero n] :
    SimplyConnectedSpace (stdSimplex ℝ (Fin n)) :=
  inferInstance

/-- **Fiber of the trigonometric covering.**  `trigCirclePoint a = trigCirclePoint b`
exactly when `a` and `b` differ by an integer number of full turns `2π`.  This is
the deck-transformation group `2π ℤ` of the universal cover `ℝ → S¹`. -/
theorem trigCirclePoint_eq_iff (a b : ℝ) :
    trigCirclePoint a = trigCirclePoint b ↔ ∃ m : ℤ, a = b + (m : ℝ) * (2 * Real.pi) := by
  rw [trigCirclePoint_eq_iff_exp, Circle.exp_eq_exp]

/-- The covering map of `TopCat.sphere 1`, repackaged as an
`IsCoveringMap` term for direct use with the path-lifting API. -/
theorem isCoveringMap_trig : IsCoveringMap CircleParam.trigCirclePoint :=
  isCoveringMap_trigCirclePoint

What this page does not claim

The module does not define the winding number itself; it establishes the lifting prerequisites. The module does not prove the circle is simply connected; it proves the standard simplex is. The module does not introduce any new axioms or project-local definitions of 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/CircleLifting.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: