Foundation Circle Covering Carrier Covering

The covering map

A covering map is a continuous function from one space onto another such that every point of the target has a neighborhood whose preimage is a disjoint union of open sets, each mapped homeomorphically onto that neighborhood. The classic example is the map from the real line to the unit circle that sends a real number t to the point (cos t, sin t). Each point on the circle has a small arc around it, and the preimage of that arc under the map is a stack of infinitely many open intervals, one for each integer multiple of 2π. This map is the backbone of winding numbers: it records how many times a loop wraps around the circle.

The map t ↦ (cos t, sin t) has been known since trigonometric functions were formalized, but proving that it is a covering map in a machine-checked library of formal theorems requires building the circle as a specific topological space and then transporting the proof through a series of equivalences. The framework's library does exactly this. It starts with the complex exponential map, already known to be a covering map from the complex plane to the unit circle in the complex numbers. An orthonormal-basis isometry sends the complex plane to the two-dimensional real Euclidean space, carrying the unit circle to the metric unit circle. A homeomorphism then moves the result onto the exact topological space known as the unit sphere in two dimensions. The composition of these equivalences yields the concrete map carrierCovering, and a theorem proves it is a genuine covering map of that sphere.

In Recognition Science, this covering map is the foundation for the winding and degree invariant on singular 1-chains. The framework's library needed this invariant to prove that the first homology group of the circle is the integers, a result that standard homology theory only proves for totally disconnected spaces. The covering map provides the lifting property: a path in the circle can be lifted to a path in the real line, and the difference between the endpoints of the lift measures the winding. The theorem that the trigonometric parametrization is a covering map is the hinge that makes this invariant well-defined.

The declaration carrierCovering is the concrete function itself, defined as the composition of the circle homeomorphism with the complex exponential. Its companion theorem isCoveringMap_carrierCovering states that this function is indeed a covering map. A further result, carrierCovering_val, shows that the map agrees pointwise with the trigonometric vector (cos t, sin t). These are exact statements about a specific topological object, not about a general principle.

What the declaration does not claim is equally precise. It does not assert that the circle has any particular homology group; that is a separate theorem built on top of the covering map. It does not claim that the map is unique or that it is the only covering map of the circle. It does not make any statement about the framework's recognition cost function or its forcing chain; the covering map is a piece of standard topology, imported and verified, not a new physical law. The declaration is a tool, not a conclusion.

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

/-- The carrier covering agrees with the ambient trigonometric vector
`(cos t, sin t)`. -/
theorem carrierCovering_val (t : ℝ) :
    (carrierCovering t : SphereOneAmbient) = trigCircleVector t := by
  show isoE (Circle.exp t : ℂ) = trigCircleVector t
  rw [show (Circle.exp t : ℂ) = Complex.exp (t * Complex.I) from Circle.coe_exp t,
      show isoE (Complex.exp (t * Complex.I))
        = Complex.orthonormalBasisOneI.repr (Complex.exp (t * Complex.I)) from rfl]
  ext i
  rw [Complex.orthonormalBasisOneI_repr_apply]
  fin_cases i
  · simp [trigCircleVector, Complex.exp_ofReal_mul_I_re]
  · simp [trigCircleVector, Complex.exp_ofReal_mul_I_im]

What this page does not claim

The declaration does not prove that the first homology group of the circle is the integers. It does not assert that the covering map is unique among all covering maps of the circle. It makes no statement about the framework's recognition cost function or its physical forcing chain.

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: