Foundation Circle Covering Iso E

The circle's coordinate bridge

The complex plane and the ordinary Euclidean plane are different arenas for the same circle. The complex unit circle is the set of points at distance one from zero in the complex numbers; the Euclidean unit circle lives in the real two-dimensional plane. The declaration isoE is the formal bridge between them: a structure-preserving bijection that sends each complex number on the unit circle to its real coordinate pair, preserving distances, angles, and the group structure. It is written as an isometry, meaning it preserves the metric, and it is built from the standard orthonormal basis of the complex numbers as a real vector space.

The point of this bridge is not the bridge itself but what it lets the library prove. With isoE, the library transports a known result about the complex exponential map to the exact metric circle in the topological sphere object. The concrete map t ↦ (cos t, sin t), the familiar trigonometric parametrization, becomes a covering map: every point on the circle has a neighborhood that lifts evenly to a disjoint union of open intervals in the real line. This is the foundation for defining a winding number or degree invariant on singular chains, the tool that ultimately computes the first homology group of the circle as the integers.

The declaration itself is a definition, not a theorem. It chooses a specific identification, the one coming from the standard basis, and it does not claim uniqueness. Other isometries between the two circles exist, for example rotations of the plane, and isoE is one canonical choice among them. What the surrounding theorems establish is that this particular choice makes the trigonometric parametrization a genuine covering map, with no axioms or project-local replacements for the circle. The result is about the imported topological sphere object through real equivalences, not about a simplified or custom-built circle.

In Recognition Science, this is the covering-space foundation for the by-hand derivation of the circle's first homology group. Mathlib's singular-homology development proves nothing beyond the totally-disconnected case, so every route to H₁(S¹; ℤ) ≅ ℤ must build its own degree invariant, and the invariant is defined by lifting singular simplices through a covering map. isoE makes that lifting possible on the exact carrier object. The framework's library uses this to establish a structural fact about the circle that classical algebraic topology already knows; the contribution is the clean, machine-checked route, not a new mathematical discovery about the circle itself.

/-- The orthonormal-basis isometry `ℂ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 2)`. -/
def isoE : ℂ ≃ₗᵢ[ℝ] SphereOneAmbient :=
  Complex.orthonormalBasisOneI.repr

/-- **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 transported map is a genuine covering map of the metric circle carrier. -/
theorem isCoveringMap_carrierCovering : IsCoveringMap carrierCovering :=
  Circle.isCoveringMap_exp.homeomorph_comp circleHomeoCarrier

What this page does not claim

isoE is the unique isometry between the two circles; it is a canonical choice, not the only one. The declaration itself proves the covering map property; that is the work of the surrounding theorems. The framework derives a new fact about the circle's topology; the result is a machine-checked route to a classical fact.

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: