Foundation Circle Covering Circle Homeo Carrier

The circle's exact shape

A circle is a set of points at a fixed distance from a center. The unit circle in the plane is the set of points (x, y) with x² + y² = 1. There is also an abstract circle, often written as the set of complex numbers with absolute value 1. These two descriptions look different, but topologically they are the same shape. A homeomorphism is a continuous, reversible stretching that proves two spaces are topologically identical.

The declaration circleHomeoCarrier is a formal construction in the framework's machine-checked library of formal theorems. It builds an explicit homeomorphism between the abstract circle and the unit circle in the plane. The map sends a complex number z on the unit circle to the real pair (Re z, Im z). This is a bijection, it is continuous in both directions, and its inverse is the map (x, y) ↦ x + iy. The construction is not a new idea; it is a formal verification that the standard identification is a genuine homeomorphism.

The declaration is a definition, not a theorem. It defines the homeomorphism, but it does not prove that the map is a homeomorphism. The proof is a separate theorem, isCoveringMap_carrierCovering, which shows that the trigonometric parametrization t ↦ (cos t, sin t) is a covering map of the unit circle. A covering map is a continuous surjection where each point has a neighborhood that is evenly covered by disjoint open sets. This is a stronger property than being a homeomorphism, and it is the foundation for defining the winding number of a loop around the circle.

In Recognition Science, this homeomorphism is a technical step. It identifies the abstract circle used in the framework's internal constructions with the concrete unit circle in the plane. This identification is needed to transfer results about covering maps from one setting to the other. The framework's library proves that the trigonometric parametrization is a covering map, and this is used to define a degree invariant for singular chains on the circle. The homeomorphism itself is the bridge that makes this transfer possible.

The declaration does not claim that the homeomorphism is unique, nor that it is the only way to identify the two circles. It does not claim that the unit circle is the only circle, nor that all circles are homeomorphic to it. It does not claim that the covering map is the only covering map of the circle. The declaration is a specific, explicit construction, and its value is that it is machine-checked. It provides a solid foundation for the framework's later results about the circle's homology.

/-- The induced homeomorphism from Mathlib's `Circle` onto the exact metric
unit-circle carrier of `TopCat.sphere 1`. -/
def circleHomeoCarrier : Circle ≃ₜ SphereOneCarrier :=
  Homeomorph.subtype isoE.toHomeomorph (fun z => by
    show z ∈ Metric.sphere (0 : ℂ) 1 ↔
        (isoE.toHomeomorph z) ∈ Metric.sphere (0 : SphereOneAmbient) 1
    simp only [Metric.mem_sphere, dist_zero_right, LinearIsometryEquiv.coe_toHomeomorph,
      LinearIsometryEquiv.norm_map])

/-- The transported map is a genuine covering map of the metric circle carrier. -/
theorem isCoveringMap_carrierCovering : IsCoveringMap carrierCovering :=
  Circle.isCoveringMap_exp.homeomorph_comp circleHomeoCarrier

/-- **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

What this page does not claim

The homeomorphism is not claimed to be unique or canonical. The covering map is not claimed to be the only covering map of the circle. The declaration does not prove that the unit circle is the only 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/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: