Foundation Circle Covering Ulift Carrier Covering Eq Trig

The trigonometric covering

The unit circle in the plane is usually described by the parametrization t ↦ (cos t, sin t). This declaration establishes a precise topological property of that map: it is a covering map. A covering map is a continuous function where every point in the target has a neighborhood that is evenly covered by disjoint open pieces of the source. For the circle, this means that near any point on the circle, the real line looks like a stack of identical intervals, each mapping down to the same arc. The result is proved in the framework's machine-checked library of formal theorems, using real equivalences and no extra axioms.

The statement itself, ulift_carrierCovering_eq_trig, is a technical equality. It says that a certain map built from the complex exponential, transported through a homeomorphism into the exact carrier of the topological circle, is pointwise equal to the familiar trigonometric parametrization. The homeomorphism is an isometry between the complex numbers and the real plane, and the carrier is the metric unit circle. The equality is not a new geometric fact; it is a bridge. It connects the abstract covering map, constructed from the exponential, to the concrete formula that appears in every trigonometry course.

In Recognition Science, this bridge matters because the framework needs a winding number. The winding number counts how many times a loop goes around the origin, and it is defined by lifting the loop through a covering map. Mathlib's singular-homology development proves nothing beyond the totally-disconnected case, so the framework builds its own invariant. The headline theorem, isCoveringMap_trigCirclePoint, states that the trigonometric parametrization itself is a covering map. The equality ulift_carrierCovering_eq_trig is the step that makes this theorem true for the exact object TopCat.sphere 1, not just for a convenient model.

The declaration does not claim that the trigonometric parametrization is the only covering map, nor that it is a universal cover in a sense that would require the real line to be simply connected. It does not claim anything about the winding number's properties, such as its invariance under homotopy or its integrality; those are separate results. It also does not claim that the covering map is unique or that the framework's approach to homology is simpler than the standard one. The declaration is a foundation stone, not a building.

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

This declaration does not prove the winding number is an integer or that it is homotopy invariant. It does not claim the trigonometric parametrization is the unique covering map of the circle. It does not assert that the framework's approach to homology is simpler or better than the standard development.

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: