IndisputableMonolith.Foundation.CircleCovering
Sets up the standard covering map from the real line onto the unit circle, identified with the imported TopCat.sphere 1 carrier via the C ≃ R² isometry. Supplies the homeomorphism of carriers and proves the trigonometric projection is a covering map. Cited by the circle-lifting layer that builds the winding/degree invariant on singular 1-chains. The argument is classical covering-space bookkeeping glued to Mathlib's Circle and Covering APIs.
claimIdentify $\mathbb{C}\simeq_{\mathbb{R}}\mathbb{R}^2$ by the orthonormal-basis linear isometry, transport the unit circle carrier, and obtain a covering map $\mathbb{R}\to S^1$ whose underlying map is the standard trigonometric projection $t\mapsto(\cos t,\sin t)$, equal (after the carrier homeomorphism and universe lift) to the circle map used on $\mathrm{TopCat.sphere}\,1$.
background
Recognition Science's foundation layer derives the first homology of the circle by hand against the actual imported object TopCat.sphere 1, rather than a custom model. The upstream module CircleParam fixes the exact carrier, a checked basepoint, and the constant singular 1-simplex face identities in TopCat.toSSet.obj (TopCat.sphere 1). Those primitives stop short of a covering map.
This module supplies the missing geometric bridge. It introduces the orthonormal-basis isometry $\mathbb{C}\simeq_{\ell i[\mathbb{R}]}\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin},2)$, the homeomorphism of circle carriers, and the covering map obtained by transporting the classical real-line cover of the unit circle. Mathlib's Circle, PiL2, and Topology.Covering APIs are the ambient toolkit; the local work is identification and equality of maps, not a new covering theorem.
proof idea
Definition-heavy module with short covering proofs. First define the real-linear isometry from $\mathbb{C}$ onto $\mathbb{R}^2$ on the standard orthonormal frame. Transport the unit-circle carrier along that isometry to obtain a homeomorphism of carriers. Package the standard trigonometric projection as a map into the transported carrier, then verify it is a covering map by Mathlib's covering criteria. Finally identify the universe-lifted carrier covering with the trigonometric circle-point map, so the named covering isCoveringMap_trigCirclePoint is literally the classical cover on the imported sphere object.
why it matters in Recognition Science
Feeds Foundation.CircleLifting, whose doc-comment states that the winding/degree invariant on singular 1-chains of TopCat.sphere 1 is built by lifting singular simplices through CircleCovering.isCoveringMap_trigCirclePoint. Without a checked covering map on the exact imported carrier, the lift of 1-simplices (and thus the integer winding number) cannot be defined inside the by-hand H1 derivation.
In the broader Recognition chain this is infrastructure, not a forcing step: it underwrites the topological side of the eight-tick/octave story (period structures on the circle) once homology and degree are available. It closes no T0–T8 obligation by itself; it makes the circle's covering geometry usable downstream of CircleParam and upstream of the lifting and winding modules.
scope and limits
- Does not compute H₁(S¹) or define the winding number on chains.
- Does not prove uniqueness of lifts; that lives in CircleLifting.
- Does not treat higher spheres or non-trigonometric circle models.
- Does not address RS forcing steps T0–T8 or physical constants.
- Does not replace Mathlib covering theory; only identifies the imported carrier.