continuous_trigCircleVector
plain-language theorem explainer
The ambient map sending a real angle to the Euclidean vector (cos t, sin t) is continuous. Anyone assembling continuous singular 1-simplices or once-around loops on Mathlib's TopCat.sphere 1 cites this fact. The argument is a short composition: PiLp continuity of the ℓ² embedding with the standard continuity of cosine and sine on each coordinate.
Claim. The map $t \mapsto (\cos t, \sin t)$ from $\mathbb{R}$ into the ambient Euclidean space $\mathbb{R}^2$ (equipped with the $\ell^2$ product structure used by Mathlib's unit circle) is continuous.
background
This module builds circle-parametrization primitives by hand against the imported TopCat.sphere 1 object. It fixes the exact ambient Euclidean space (the $\ell^2$ product $\mathbb{R}^2$), a checked basepoint on the metric unit circle, and the 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 are meant to live in the same singular set and use the same face maps.
The ambient trigonometric vector is the standard parametrization $t \mapsto (\cos t, \sin t)$ valued in that Euclidean plane. Continuity of this ambient map is the first analytic step before lifting into the metric sphere subtype and then into the ULift wrapper that Mathlib uses for TopCat.sphere 1.
proof idea
Rewrite the goal so the codomain is explicitly the WithLp/PiLp presentation of the ambient Euclidean space. Apply Mathlib's continuity of the map into PiLp at $p=2$, composed with continuous_pi on the two coordinates. Case-split on the Fin 2 index: the first coordinate is continuous by Real.continuous_cos, the second by Real.continuous_sin (each simplified into place).
why it matters
This is the ambient continuity lemma that the once-around sphere map needs. Downstream, continuity of the trigonometric point in the exact TopCat.sphere 1 object is obtained by composing this result with subtype and ULift continuity. That parent theorem is the analytic gate for placing a genuine once-around singular 1-simplex inside TopCat.toSSet.obj (TopCat.sphere 1), which is the module's stated first step toward a by-hand circle-$H_1$ derivation. In the broader Recognition foundation stack this is pure topological scaffolding: it does not yet touch the forcing chain (T0–T8), the J-cost, or the eight-tick octave, but it supplies the continuous circle generator those later geometric constructions will sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.