orientedEdgePath_zero
plain-language theorem explainer
For any oriented singular edge on S¹, the path it induces on the unit interval starts at the circle point of its oriented initial vertex. Anyone assembling closed walks or checking cyclic connectivity of oriented edges cites this endpoint identity. The proof is a two-case split on orientation, reducing to the unoriented edge-path endpoint lemmas plus path reversal at t=0.
Claim. Let $o$ be a singular $1$-simplex of $S^1$ equipped with a traversal orientation. The continuous path $I\to S^1$ associated to $o$ satisfies $\gamma_o(0)=v_{\mathrm{init}(o)}$, where $v_{\mathrm{init}(o)}$ is the $S^1$-point of the oriented initial $0$-simplex of $o$.
background
This module lifts the path-level winding and displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that displacement kills boundaries of $2$-simplices. That identity, with the generator evaluation on the fundamental loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
An oriented singular edge pairs a singular $1$-simplex with a forward or backward orientation. Its initial vertex is the edge's initial $0$-face when forward, and the terminal $0$-face when backward. The associated path is the standard singular-edge path, or that path reversed. The map vertexPoint extracts the actual point of $S^1$ carried by a singular $0$-simplex.
Upstream, the unoriented path meets the initial and terminal vertices at the endpoints $0$ and $1$, and reversing a path evaluates as $\gamma(1-t)$. Those facts pin the oriented initial endpoint.
proof idea
Destructure the oriented edge into its underlying singular edge and orientation, then case on orientation.
Forward case: the oriented path is the singular edge path, and the oriented initial vertex is the edge's initial face, so the claim is exactly the unoriented initial-endpoint lemma.
Backward case: the oriented path is the reverse of the singular edge path, so at $t=0$ one applies the reverse-path evaluation identity and $1-0=1$, reducing to the unoriented terminal-endpoint lemma; the oriented initial vertex is that terminal face.
why it matters
Oriented closed walks need matching path endpoints at each cyclic glue: the terminal of one oriented edge must equal the initial of the next. This lemma is the initial half of that glue; together with the companion terminal-endpoint statement it feeds orientedWindingSum_cyclic_integral, which proves that a cyclically connected family of oriented edges has integer total oriented winding.
Downstream it also appears in the structure of concrete oriented cyclic families and in the terminal-side correction generation theorem that builds an explicit $2$-chain closing those families. In the module's larger program, integer winding on cycles is the left inverse to the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation (surjectivity) half still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.