singularTwoBoundaryFree_coneSingularTwoChainOfPathFamily
plain-language theorem explainer
For a finite family of paths on the circle, the free singular boundary of their summed cone 2-chain equals the sum of terminal-return edges, minus the sum of constant apex edges, plus the sum of the base path edges. Anyone building multi-edge prism telescoping or oriented cyclic families on S¹ cites this shell identity. The proof unfolds the family sum, pushes the boundary through it, and applies the single-path cone boundary lemma termwise.
Claim. Let $\gamma : \mathrm{Fin}\,k \to C(I,S^1)$ be a finite family of continuous paths on the circle. The image of the summed cone $2$-chain of $\gamma$ under the free singular boundary map equals $\sum_i [\mathrm{terminal\text{-}return}(\gamma_i)] - \sum_i [\mathrm{const}_{\gamma_i(0)}] + \sum_i [\gamma_i]$, where each bracket denotes the corresponding free generator singular $1$-simplex.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\partial_0 F)-\mathrm{disp}(\partial_1 F)+\mathrm{disp}(\partial_2 F)=0$. That identity is the chain-level fact making winding a homology invariant and supplying the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A cone over a path $\gamma$ is a singular $2$-simplex whose faces are the base path (read as a $1$-simplex via $\Delta^1\simeq I$), a constant edge at the apex $\gamma(0)$, and a terminal-return side that closes the cone using the path lift. The family version sums these free generators over $\mathrm{Fin},k$. The free boundary map is the linear map on free singular chains that sends each generator to its alternating face sum.
The single-path identity already computes the boundary of one cone: terminal-return minus constant apex plus base path. The present statement is the finite-sum shell of that identity.
proof idea
Term-mode reduction by rewriting. Unfold the family cone chain as $\sum_i$ of single-path cone generators. Push the free boundary homomorphism through the sum via map_sum. Replace each summand by the single-path cone boundary lemma singularTwoBoundaryFree_freeMk_coneSingularTwoSimplexOfPath, which expands one cone into terminal-return minus constant apex plus base path. Finish by distributing the outer sum over addition and subtraction (Finset.sum_add_distrib, Finset.sum_sub_distrib) to obtain the three separate family sums.
why it matters
This is the algebraic target whose side terms must telescope in the multi-edge prism, as the doc-comment states. Downstream it feeds OrientedCyclicFamilyTerm, the concrete oriented cyclic family: a finite sign-oriented closed walk in singular $1$-simplices with matching terminal/initial vertices under cyclic rotation. That structure is the combinatorial carrier for closed multi-edge walks whose cone shells cancel on internal edges.
In the module's larger program, winding on singular $1$-simplices plus the kills-boundaries identity give a left inverse to the fundamental class on $H_1(S^1)$. Surjectivity (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply. The finite-family cone shell is a necessary bookkeeping step toward that prism cancellation, not a framework T0–T8 landmark itself, but foundation infrastructure for the circle's homology comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.