continuous_trigCirclePoint
plain-language theorem explainer
The standard angle map t ↦ (cos t, sin t) is continuous as a map from ℝ into the exact topological 1-sphere object used by the singular-set API. Anyone building once-around paths, fundamental loops, or cone simplices on S¹ cites this. The proof unfolds the ULift/subtype packaging and composes the already-proved ambient continuity with the continuous ULift and subtype constructors.
Claim. The once-around trigonometric parametrization $t \mapsto (\cos t, \sin t)$, packaged as a point of the exact topological space $S^1 = \mathrm{TopCat.sphere}\,1$, is a continuous map $\mathbb{R} \to S^1$.
background
Module CircleParam begins a by-hand $H_1(S^1)$ derivation against the imported TopCat.sphere 1 object. It fixes the exact carrier, a checked basepoint, and constant singular 1-simplex face identities in the singular simplicial set of that sphere. The constant simplex is only an API anchor; later once-around simplices must live in the same singular set and use the same face maps.
The ambient map trigCircleVector sends $t \in \mathbb{R}$ to the $\ell^2$ vector $(\cos t, \sin t)$ in the ambient Euclidean plane of the unit sphere. Continuity of that ambient map is already proved. The point-level map packages each ambient value as a subtype point of the unit sphere and then lifts it into the TopCat.sphere 1 object via ULift.up. Continuity of the packaged map is the statement needed by every downstream continuous path or simplex into that exact object.
proof idea
One-line term proof after unfolding the definition of the packaged map. Continuity of the ambient trigonometric vector map is composed with the continuous subtype constructor (membership in the unit sphere is already checked pointwise) and then with continuous ULift.up. No separate $\varepsilon$-$\delta$ work is done here; all analytic content sits in the ambient continuity lemma.
why it matters
This is the continuity hinge for the circle-parametrization stack. Downstream, the fundamental once-around path map on the standard 1-simplex, the fundamental loop $I \to S^1$, cone terminal sides, geodesic 1-simplices, and linear 2-simplex maps all obtain continuity by composing with this theorem. Winding and homotopy results (zero-winding loops null-homotopic rel endpoints; cone apex limits) likewise route through it when they project lifted real angles back to the exact sphere object.
In the Recognition foundation layer this is infrastructure, not a forcing-chain step: it makes the singular-set model of $S^1$ usable so later once-around generators and winding arguments can be stated against the real TopCat.sphere 1 rather than an ad-hoc carrier. No T0–T8 landmark is discharged here; the gain is a checked continuous covering-style parametrization for the circle API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.