fundamentalSphereOneSingularOneSimplex_faces_eq
plain-language theorem explainer
The once-around singular 1-simplex on the circle is a loop: its two endpoint faces coincide at the chosen basepoint in the singular simplicial set of S¹. Anyone building the generator for singular H₁(S¹) cites this equal-faces fact. The proof is a one-line rewrite through the two face evaluations, each already identified with the constant 0-simplex.
Claim. Let $\sigma$ be the once-around singular $1$-simplex in the singular simplicial set of the topological $1$-sphere $S^1$. Then the two face maps agree: $\delta_0(\sigma)=\delta_1(\sigma)$.
background
This module builds the geometric once-around singular 1-simplex inside the actual singular simplicial set TopCat.toSSet.obj (TopCat.sphere 1), not a combinatorial model. The simplex is obtained by transporting the standard angle path map on the circle through the singular-set equivalence, so it is the candidate geometric generator for later H₁ work.
In Mathlib's simplex convention, the face $\delta_0$ evaluates the second barycentric coordinate at 1 (angle $2\pi$), while $\delta_1$ evaluates it at 0 (angle 0). Both endpoints land on the same chosen basepoint of $S^1$, recorded as the constant singular 0-simplex. The two face theorems state exactly those endpoint identities.
proof idea
One-line term-mode rewrite. Apply the face-zero theorem (identifying $\delta_0(\sigma)$ with the constant basepoint 0-simplex) and the face-one theorem (identifying $\delta_1(\sigma)$ with the same constant 0-simplex). Transitivity of equality yields $\delta_0(\sigma)=\delta_1(\sigma)$. No further topology is invoked.
why it matters
Equal faces are the geometric content of a closed loop. Downstream, the chain-level theorem fundamentalSphereOneSingularOneChain_boundary_zero quotes this fact to show that the fundamental singular 1-chain has vanishing boundary in the singular chain complex of $S^1$. That zero-boundary statement is the first algebraic step toward computing $H_1(S^1)\cong\mathbb{Z}$ from the geometric generator.
In the Recognition Science foundation layer this sits under the circle-parametrization infrastructure that later supports discrete octave and eight-tick constructions; the present lemma itself is pure singular topology and does not yet invoke J-cost, $\phi$, or the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.