trigCirclePoint
plain-language theorem explainer
Packages the standard map $t\mapsto(\cos t,\sin t)$ as a point of Mathlib's exact topological sphere $S^1$. Anyone building covering maps, once-around singular 1-simplices, or path-lifting on that object cites this constructor. The body is a one-line subtype-plus-ULift wrapper around the ambient Euclidean vector and its unit-sphere membership proof.
Claim. For each real number $t$, the point $(\cos t,\sin t)$ on the Euclidean unit circle, viewed as an element of the topological $1$-sphere object $S^1$ in $\mathbf{Top}$.
background
The module builds circle-$H_1$ primitives against Mathlib's imported TopCat.sphere 1, not a custom model. 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 generators must live in the same simplicial set and use the same face maps.
Upstream, the ambient Euclidean vector $(\cos t,\sin t)$ is defined in the $2$-dimensional Euclidean space underlying the metric unit sphere, and a short norm computation shows it lies on that sphere: $|(\cos t,\sin t)|=1$. The topological sphere object is the ULift of that metric sphere subtype, so points must be packaged through that lift.
proof idea
Pure definitional packaging. Form the subtype pair of the ambient trigonometric vector with the membership theorem that places it on the metric unit sphere, then apply ULift.up so the result inhabits the exact TopCat.sphere 1 type. No further algebraic work.
why it matters
This is the shared point-level API for the circle covering and fundamental-simplex stack. Downstream, the covering theorem states that $t\mapsto(\cos t,\sin t)$ is a covering map of the imported $S^1$, giving the winding/degree foundation on singular $1$-chains. A companion identity shows the carrier covering, after ULift, equals this map pointwise. The fundamental once-around path map is defined by composing this constructor with the second barycentric coordinate scaled by $2\pi$, and the face identities for the fundamental singular $1$-simplex evaluate endpoints at angles $0$ and $2\pi$ through it. Path-lifting re-exports the covering property under this name. In the Recognition foundation layer this is infrastructure for $H_1(S^1)$, not a physics forcing step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.