trigCirclePoint_two_pi
plain-language theorem explainer
The standard angle map on the unit circle sends $2\pi$ back to the chosen basepoint of Mathlib's $S^1$. Anyone building singular simplices or face identities for the once-around generator cites this closure. The proof peels the ULift/Subtype packaging and simplifies the two Euclidean coordinates with the usual cosine/sine values at a full turn.
Claim. The trigonometric point map $t \mapsto (\cos t, \sin t)$ on Mathlib's unit circle $S^1$ satisfies $\gamma(2\pi) = p_0$, where $p_0$ is the fixed basepoint corresponding to the first coordinate unit vector $(1,0)$.
background
This module builds circle-parametrization primitives against the imported TopCat.sphere 1 object: exact carrier, checked basepoint, and constant singular 1-simplex face identities in the singular simplicial set. 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 plane is Euclidean 2-space. The base vector is the first coordinate unit vector $(1,0)$; the basepoint is that vector packaged as a point of TopCat.sphere 1. The trigonometric vector at angle $t$ is $(\cos t, \sin t)$, and the trigonometric point is the same data lifted into the sphere object. Continuity and sphere-membership of these maps are already recorded upstream.
The identity at a full turn is the elementary closing relation needed before face maps of a once-around singular 1-simplex can be identified with the constant 0-simplex at the basepoint.
proof idea
Term-mode proof by successive extensionality. Apply ULift.ext then Subtype.ext to drop the sphere packaging down to the ambient Euclidean vector. Pointwise equality on Fin 2 coordinates is obtained by ext i and fin_cases i. Each case reduces by simp unfolding the trigonometric point/vector and the basepoint/base-vector definitions, using $\cos(2\pi)=1$ and $\sin(2\pi)=0$.
why it matters
Feeds the face identity fundamentalSphereOneSingularOneSimplex_face_zero: the $\delta 0$ face of the fundamental singular 1-simplex equals the constant 0-simplex at the basepoint. Downstream doc notes that Mathlib's simplex convention evaluates that endpoint at the second barycentric coordinate $1$, hence at angle $2\pi$. Without this return-to-basepoint fact, the once-around generator cannot be glued consistently in TopCat.toSSet.obj (TopCat.sphere 1).
In the broader Recognition foundation this is scaffolding for a by-hand $H_1(S^1)$ computation against the real Mathlib sphere, not a physics forcing step. It does not itself invoke the eight-tick octave or $D=3$; it only locks the geometric period of the circle model those later constructions will use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.