edgeTerminal
plain-language theorem explainer
Extracts the terminal (ending) vertex of a singular 1-simplex on S¹ by applying the face map δ₀. Anyone building free 1-chains, incidence coefficients, or cyclic edge families cites it as the positive boundary endpoint. The body is a one-line face-operator application in the singular simplicial set of the circle.
Claim. For a singular $1$-simplex $e$ on $S^1$, the terminal vertex is the $0$-face $\delta_0(e)$, a singular $0$-simplex on $S^1$. This is the endpoint that receives coefficient $+1$ in the free boundary $\partial e = \mathrm{terminal}(e) - \mathrm{initial}(e)$.
background
The module lifts path-level winding on the circle to singular simplices of TopCat.sphere 1 and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is a continuous map $\Delta^1\to S^1$ in the singular simplicial set; a singular $0$-simplex is a point of $S^1$. Face maps $\delta_i$ of that simplicial set send a $1$-simplex to its endpoints. By the standard simplex convention, $\delta_0$ hits the vertex opposite index $0$, i.e. the terminal endpoint, while $\delta_1$ hits the initial endpoint.
The free boundary of a generator $\langle e\rangle$ is therefore $\mathrm{terminal}(e)-\mathrm{initial}(e)$. Incidence coefficients, oriented edges, and cyclic connectivity hypotheses are all phrased in terms of these two vertices.
proof idea
One-line definition: apply the singular face operator $\delta$ at index $0\in\mathrm{Fin},2$ in the singular simplicial set of the topological $1$-sphere. No lemmas or tactics; pure face-map evaluation.
why it matters
This is the positive endpoint primitive for the whole free-chain calculus on the circle. Downstream, incidenceCoeff sets $+1$ exactly when the vertex equals the terminal; cyclicEdgeFamily_freeBoundary_zero uses terminal-equals-next-initial connectivity to prove free-boundary vanishing for cyclic families; directedCycleFreeTerm_of_cyclicFamily packages that vanishing into genuine degree-$1$ cycles with integer winding; positivity and sign-selection lemmas (edgeContribution_pos_at_oriented_terminal, initial_eq_of_negative_edgeContribution) read oriented terminals to force compensating edges in balanced flows.
In the module narrative this supplies the combinatorial half of the winding homomorphism on $1$-cycles (the left inverse to the fundamental class). It does not itself touch the forcing chain T0–T8 or the Recognition Composition Law; it is pure singular-homology scaffolding for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.