singularEdgePath_zero
plain-language theorem explainer
The unit-interval path attached to a singular 1-simplex on S¹ starts at the S¹-point of that simplex's initial 0-face. Anyone matching chain-level edges to path-level winding or displacement cites this endpoint identity. The proof unfolds the path construction, uses the standard homeomorphism Δ¹ ≃ I at 0, and applies the face-map endpoint lemma.
Claim. For every singular $1$-simplex $s$ on $S^1$, if $\gamma_s:I\to S^1$ is the path obtained by reparameterizing $s$ through the standard homeomorphism $\Delta^1\simeq I$, then $\gamma_s(0)$ equals the underlying point of $S^1$ corresponding to the initial $0$-face $\partial_1 s$.
background
This module lifts the path-level winding and displacement invariants of the circle to singular simplices of $S^1$, and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity, with the generator sending the once-around loop to winding $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. Reading it as a continuous path $I\to S^1$ is done by composing with the standard homeomorphism that sends the unit interval onto $\Delta^1$. The initial $0$-face is the face operator $\delta_1$, matching the negative boundary term of a directed edge. The companion map vertexPoint extracts the underlying point of $S^1$ from a singular $0$-simplex.
Upstream, intervalToSimplex_zero records that the homeomorphism sends $0\in I$ to the $0$-vertex of $\Delta^1$, and the face-endpoint lemma identifies the image of that vertex under the singular simplex with the initial face.
proof idea
Term-mode proof by unfolding the path bridge (singular edge as oneSimplexPath of the underlying continuous map), the vertex-point extractor, and the initial-face operator. Rewrite the composition at $0$ via ContinuousMap.comp_apply and intervalToSimplex_zero, so the evaluation lands on the image of the $0$-vertex of $\Delta^1$. Finish by the symmetric form of the singular face-endpoint identity, which equates that image with the $S^1$-point of $\partial_1 s$.
why it matters
Endpoint bookkeeping for the chain-to-path bridge: without matching path starts to initial faces, winding sums along walks cannot be compared to combinatorial face incidence. Downstream, the oriented-edge variants quote it to pin initial points of oriented paths; the cyclic-walk integrality theorem uses the matching of terminal of $e_i$ to initial of $e_{i+1}$ at the path level to glue displacements into a closed loop whose total winding is integral; the zero-winding null-homotopy for closed singular edges likewise needs the basepoint identification.
In the broader Recognition foundation this supports the singular form of the winding homomorphism that is left-inverse to the fundamental class on $H_1(S^1)$, the "kills boundaries" half of the circle homology computation. It does not itself touch the forcing chain T0–T8 or the J-cost; it is pure topological scaffolding for the circle invariant used later in RS geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.