Foundation Circle Covering

The circle's winding number

The winding number of a closed curve around a point counts how many times the curve travels around that point. A loop that circles once has winding number 1; a loop that circles twice has winding number 2. This integer is a basic invariant in topology, and it is the foundation for the first homology group of the circle, H₁(S¹; ℤ), which is isomorphic to ℤ.

The classical route to this invariant uses a covering map: a continuous function from the real line onto the circle such that every point on the circle has a neighborhood whose preimage is a disjoint union of open intervals, each mapped homeomorphically onto the neighborhood. The standard example is the map t ↦ (cos t, sin t), which winds the real line around the unit circle infinitely many times. Lifting a loop through this covering map and measuring the net change in t defines the winding number.

In Recognition Science, the framework's machine-checked library of formal theorems needed this same foundation for its own work on the circle. The library proves that the trigonometric parametrization t ↦ (cos t, sin t) is indeed a covering map of the unit circle. This is the theorem isCoveringMap_trigCirclePoint in the module CircleCovering. The proof transports an existing covering map from the complex exponential along an isometry between the complex plane and the two-dimensional Euclidean space, and then along a homeomorphism into the exact carrier of the unit sphere. No axioms or unfinished proofs are used; the result is fully checked.

The library also shows that this covering map agrees pointwise with the trigonometric parametrization used elsewhere in the framework. This agreement means the covering map is not an abstract construction but the concrete, familiar map from trigonometry. The framework's library can therefore use the winding number as a well-founded invariant for its singular homology development, without rebuilding the theory from scratch.

In Recognition Science, this result is part of the foundation for the framework's treatment of the circle. It establishes that the standard parametrization is a genuine covering map, which is the necessary groundwork for defining a degree or winding invariant on singular chains. This invariant is then available for the framework's later results about the circle's homology and its role in the forcing chain.

/-- **The trigonometric parametrization `t ↦ (cos t, sin t)` of the imported
`TopCat.sphere 1` object is a covering map.**  This is the covering-space
foundation for the winding / degree invariant on singular `1`-chains. -/
theorem isCoveringMap_trigCirclePoint :
    IsCoveringMap CircleParam.trigCirclePoint := by
  rw [← ulift_carrierCovering_eq_trig]
  exact isCoveringMap_carrierCovering.homeomorph_comp
    (Homeomorph.ulift (X := SphereOneCarrier)).symm

/-- The carrier covering, lifted into the exact `TopCat.sphere 1` object, equals
the `CircleParam` trigonometric parametrization pointwise. -/
theorem ulift_carrierCovering_eq_trig :
    (Homeomorph.ulift (X := SphereOneCarrier)).symm ∘ carrierCovering
      = CircleParam.trigCirclePoint := by
  funext t
  apply ULift.ext
  apply Subtype.ext
  exact carrierCovering_val t

What this page does not claim

The module does not prove the first homology group of the circle is isomorphic to ℤ. The module does not define the winding number itself, only the covering map on which it is built.

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/CircleCovering.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: