trigCirclePoint_zero
plain-language theorem explainer
The trigonometric circle map sends angle 0 to the chosen basepoint of the unit circle object. Anyone wiring face maps or singular 1-simplices for a by-hand H1(S^1) generator cites this normalization. The proof peels the ULift and subtype packaging, then simplifies the two ambient coordinates against the standard basis vector.
Claim. The trigonometric parametrization of the unit circle satisfies $\gamma(0)=p_0$, where $\gamma(t)=(\cos t,\sin t)$ as a point of the exact sphere object $S^1$, and $p_0$ is the basepoint given by the first standard basis vector $(1,0)$.
background
This module starts a by-hand circle-$H_1$ derivation against Mathlib's imported unit sphere object in topological spaces. It fixes the exact carrier, a checked basepoint, and constant singular 1-simplex face identities inside 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 space is the Euclidean plane. The base vector is the first coordinate unit vector $(1,0)$, verified to lie on the metric unit circle and packaged as the sphere basepoint. The trigonometric vector at angle $t$ is $(\cos t,\sin t)$; the corresponding sphere point is that vector lifted into the exact sphere object. Continuity of the parametrization is recorded separately.
proof idea
Both sides are points of the sphere object, each a ULift of a subtype of the ambient Euclidean plane. Apply ULift extensionality, then subtype extensionality, reducing to equality of ambient vectors. Pointwise extensionality on the $\mathrm{Fin},2$ index and fin_cases on the two coordinates, followed by simplification of the trigonometric map, basepoint, and base vector, yields $\cos 0=1$ and $\sin 0=0$ on the respective slots.
why it matters
Downstream, the $\delta 1$ face of the fundamental singular 1-simplex must equal the constant zero-simplex at the basepoint: that face evaluates the second barycentric coordinate at 0, hence the angle 0. This lemma supplies exactly that endpoint identity, so the fundamental once-around simplex is pinned to the same basepoint API as the constant simplex.
In the foundation layer it is a small but necessary normalization for a rigorous generator of $\pi_1(S^1)\cong\mathbb{Z}$ inside the singular simplicial set of the imported sphere, rather than an ad-hoc model of the circle. It does not itself close the H1 computation; it only locks the angle-zero end of the parametrization used by later face and boundary identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.