cyclicEdgeFamily_freeBoundary_zero
plain-language theorem explainer
A cyclically connected finite family of singular 1-simplices on S¹ has vanishing free boundary: the sum of free edge generators is a genuine 1-cycle. Anyone packaging closed edge-walks into homology classes cites this C₀ companion of the cyclic winding-sum integrality lemma. The proof is Finset telescoping: expand each boundary as terminal minus initial, then reindex initials onto terminals by finRotate.
Claim. Let $e_0,\ldots,e_{k-1}$ be singular $1$-simplices on $S^1$ such that the terminal vertex of $e_i$ equals the initial vertex of $e_{i+1\bmod k}$ for every $i$. Then the free singular boundary vanishes: $\partial\bigl(\sum_i\langle e_i\rangle\bigr)=0$ in the free module of singular $0$-chains.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that winding kills boundaries, the fact that makes winding a homology invariant. The long-term goal is 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$. The free $1$-boundary map sends each free generator $\langle s\rangle$ to $\langle\mathrm{terminal}\rangle-\langle\mathrm{initial}\rangle$, where terminal and initial are the two face maps $\delta_0$ and $\delta_1$. The cyclic-connection hypothesis says the family closes under the standard rotation of $\mathrm{Fin},k$: each edge ends where the next begins.
Upstream, the generator-level identity singularOneBoundaryFree_freeMk records exactly that free-boundary formula. The present lemma is the $C_0$ twin of the cyclic winding-sum integrality statement: same reindexing, applied to vertex chains rather than displacements.
proof idea
Push the free boundary through the finite sum (map_sum). On each free generator apply singularOneBoundaryFree_freeMk, so the $i$-th term becomes freeMk(terminal $e_i$) minus freeMk(initial $e_i$). Distribute the sum into two separate sums. Reindex the sum of initials by the equivalence finRotate k: the cyclic-connection hypothesis identifies initial($e_i$) with terminal($e_{\mathrm{rotate}^{-1}i}$), so after reindexing the two sums agree. Their difference is zero by sub_self.
why it matters
This is the boundary-zero half of cyclic extraction. Downstream, directedCycleFreeTerm_of_cyclicFamily packages a cyclically connected family into a DirectedCycleFreeTerm: the free edge-chain $\sum_i\langle e_i\rangle$ is a genuine degree-$1$ cycle precisely by this lemma, and that cycle has integer winding by the companion integrality result. That discharges the entire homological obligation of cyclic extraction; only the combinatorial task of finding such a family inside a balanced flow remains.
In the module's larger program, cycles are the domain on which the winding chain map is a homology invariant and a left inverse to the fundamental class. Without free-boundary vanishing, a closed edge-walk would not yet be an element of $Z_1$, so the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ could not start. The lemma is pure singular-chain algebra; it does not itself invoke the eight-tick octave or the forcing chain, but it sits in the foundation that later supports those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.