edgeInitial
plain-language theorem explainer
Extracts the initial endpoint of a singular 1-simplex on S¹ as a singular 0-simplex, via the face operator δ₁ of the singular simplicial set. Anyone building free boundaries, incidence coefficients, or cyclic edge families cites it. The body is a one-line application of the simplicial face map.
Claim. For a singular $1$-simplex $e$ on $S^1$, write $\mathrm{edgeInitial}(e)$ for the singular $0$-simplex obtained by applying the face operator $\delta_1$ of the singular simplicial set of $S^1$. This is the initial vertex of the directed edge, matching the negative term in the singular boundary $\partial e = \delta_0 e - \delta_1 e$.
background
The module lifts path-level winding on the circle to singular simplices of TopCat.sphere 1, and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is an element of the degree-$1$ object of the singular simplicial set of $S^1$; a singular $0$-simplex is the corresponding degree-$0$ object (a point of $S^1$ in the singular sense). Face operators $\delta_i$ of a simplicial set send an $n$-simplex to its $i$-th face of dimension $n-1$.
For a directed edge the algebraic boundary is terminal minus initial. The companion extractor for the terminal vertex uses $\delta_0$; this definition uses $\delta_1$ so that incidence coefficients and free boundaries line up with the standard singular chain complex.
proof idea
One-line definition: apply the face map $\delta(1:\mathrm{Fin},2)$ of the singular simplicial set of the topological $1$-sphere to the given singular $1$-simplex. No lemmas or tactics; pure face-operator selection matching the negative boundary term.
why it matters
This is the endpoint primitive for the whole directed-edge layer of the circle winding chain. Downstream, incidenceCoeff is $+1$ at the terminal and $-1$ at the initial vertex; cyclic connectivity hypotheses are written as edgeTerminal(e i) = edgeInitial(e (finRotate k i)); and cyclicEdgeFamily_freeBoundary_zero telescopes free boundaries of cyclic families to zero using exactly those equalities.
That vanishing, packaged in directedCycleFreeTerm_of_cyclicFamily, discharges the homological obligation when extracting integer-winding cycles from balanced flows. Local positivity and sign-selection lemmas (edgeContribution_pos_at_oriented_terminal, initial_eq_of_negative_edgeContribution) also read the initial vertex through this definition.
In the broader Recognition picture the module supplies the geometric half of $H_1(S^1)\cong\mathbb{Z}$ that underwrites the eight-tick octave and circle-valued phase structure; this def is the elementary face that makes oriented edges and free boundaries well-typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.