orientedEdgePath_one
plain-language theorem explainer
At parameter 1, the continuous path of an oriented singular edge lands on the circle point of that edge's oriented terminal 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 via path reversal.
Claim. For every oriented singular edge $o$ on $S^1$, the path associated to $o$ satisfies $\gamma_o(1)=v_{\mathrm{term}(o)}$, where $v_{\mathrm{term}(o)}$ is the point of $S^1$ carried by the oriented terminal $0$-simplex of $o$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that displacement kills boundaries, giving 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/backward orientation. Its path $\gamma_o$ is the standard edge path when forward, and the reverse path when backward. The terminal vertex swaps with the initial vertex under backward orientation. vertexPoint extracts the actual $S^1$ point of a singular $0$-simplex by evaluating the transported map at the unique vertex of $\Delta^0$.
Upstream, singularEdgePath_one states that an unoriented edge path ends at the terminal face point; singularEdgePath_zero states it starts at the initial face point. Reversal is pointwise $\gamma^{\mathrm{rev}}(t)=\gamma(1-t)$.
proof idea
Destructure the oriented edge into its underlying singular edge and orientation, then case on orientation.
Forward case: unfold the oriented path and terminal definitions; the claim is exactly singularEdgePath_one.
Backward case: the oriented path is the reverse of the singular edge path, and the oriented terminal is the unoriented initial vertex. Apply reversePath_apply and unitInterval.symm_one (so evaluation at $1$ becomes evaluation at $0$), then finish with singularEdgePath_zero.
why it matters
Endpoint matching is the glue for oriented cyclic families: a family is cyclically connected when the oriented terminal of edge $i$ equals the oriented initial of the next edge. Downstream, orientedWindingSum_cyclic_integral uses this identity to turn vertex equality into path-endpoint equality $(\gamma_{o_i}(1)=\gamma_{o_{\sigma i}}(0))$, which forces the total oriented winding of a closed walk to be an integer.
That integrality feeds OrientedCyclicFamilyTerm and the terminal-side correction generation theorem, which assemble explicit $2$-chains witnessing that oriented cyclic families are boundaries up to winding. In the module's larger program, this is part of making simplex displacement a homology invariant and obtaining a left inverse to the fundamental class on $H_1(S^1)$. It does not itself close the generation/surjectivity half (still blocked on simplicial prism/subdivision in Mathlib).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.