fundamentalSphereOneSingularOneSimplex_face_one

This module constructs the once-around singular 1-simplex inside the actual singular simplicial set of the topological circle and proves both faces land at the chosen basepoint.

The continuous path map sends a point of the standard 1-simplex to $S^1$ by reading the second barycentric coordinate $t$ and evaluating the trigonometric embedding at angle $2\pi t$. Endpoints therefore hit angles $0$ and $2\pi$. The singular 1-simplex is that path, transported by the singular-set equivalence. The constant 0-simplex is the constant map at the basepoint of $S^1$.

Upstream, the identity that the trigonometric parametrization at angle $0$ recovers the basepoint is already recorded; the face-zero companion of the present lemma handles the other endpoint.

Apply injectivity of the singular-set equivalence in dimension 0, then extensionality on the underlying continuous map. After unfolding the singular face, the path map, and the constant 0-simplex, the goal is that the trigonometric point at angle $2\pi$ times the second barycentric coordinate of $\delta_1 x$ equals the basepoint. The simplex-category face $\delta_1$ forces that second coordinate to $0$ (via the coe formula for the standard-simplex map and the explicit action of $\delta$). Finish by the upstream identity that the trigonometric parametrization at $0$ is the basepoint.

Paired with the face-zero identity, this lemma discharges the rewrite in the parent result that the two faces of the once-around singular 1-simplex coincide, so the simplex is a loop in the singular simplicial set of $S^1$. That loop is the geometric generator candidate for the later $H_1$ computation on the circle. In the Recognition foundation layer it supplies the topological circle's fundamental class before cost functionals or the forcing chain (T0–T8) enter.