trigCircleVector
plain-language theorem explainer
The ambient Euclidean vector $(\cos t,\sin t)$ in the exact 2-dimensional Euclidean space underlying Mathlib's metric unit circle. Anyone building continuous maps, basepoints, or singular 1-simplices into $\mathrm{TopCat.sphere}\,1$ cites this as the raw trigonometric parametrization. It is a one-line definition via the Euclidean-space constructor from cosine and sine.
Claim. For each real $t$, define the ambient vector $(\cos t,\sin t)$ in the Euclidean space $\mathbb{R}^2$ that is the ambient space of Mathlib's metric unit circle $S^1$ (i.e., $\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,2)$).
background
The module begins a by-hand circle-$H_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 type is the Euclidean space $\mathbb{R}^2$ (Fin 2 coordinates) that Mathlib uses for the metric sphere of radius 1. The trigonometric map $t\mapsto(\cos t,\sin t)$ is the classical parametrization of that unit circle in ambient coordinates, before any subtype or ULift packaging into the topological sphere object.
proof idea
One-line definition: construct the ambient Euclidean vector by the two-component EuclideanSpace notation with components $\mathrm{Real.cos},t$ and $\mathrm{Real.sin},t$. No lemmas are applied; the body is pure data construction.
why it matters
This is the raw ambient parametrization that the rest of the circle API sits on. Downstream, membership on the metric unit sphere is checked separately; continuity of the ambient map is proved; the packaged point in TopCat.sphere 1 is built by lifting the subtype; basepoint identities at $0$ and $2\pi$ are stated; and the carrier covering is shown to agree with this trigonometric vector. In the Recognition foundation stack it supplies the concrete once-around generator material for the singular-set $H_1$ comparison against Mathlib's sphere, which is the geometric side of the eight-tick / circle forcing story (period identification on $S^1$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.