cyclicSingularEdgeListTermListChain
plain-language theorem explainer
Sums a finite list of concrete cyclic edge-list pieces into one free singular 1-chain on S¹: empty list is zero; each term contributes its integer coefficient times the unit-coefficient edge-list chain. Anyone proving that balanced free edge-flows decompose into cyclic pieces cites this as the target assembly map. The body is a straightforward recursive list fold.
Claim. Given a finite list of concrete cyclic edge-list terms (each an edge list of singular $1$-simplices, a global integer coefficient, and a certified cycle whose free-chain image equals that coefficient times the listed edge sum), form the free singular $1$-chain equal to the sum over the list of $\mathrm{coeff}_i \cdot \sum_j e_{i,j}$. The empty list maps to $0$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The free module singularOneChainFree is the free $\mathbb{Z}$-module on actual singular $1$-simplices of $\mathrm{TopCat.sphere},1$.
A concrete cyclic edge-list term packages a finite list of singular $1$-simplices, a global integer coefficient, a cycle in the singular chain complex, a certificate that the free image of that cycle equals the coefficient times the listed edge sum, and an integrality witness for the winding. The helper singularEdgeListChain turns a bare edge list into the free chain with coefficient $1$ on each simplex (empty list to $0$, cons as free generator plus recursive sum).
This definition is the list-level assembly of those pieces: it is the concrete target type for statements that every free $1$-chain with vanishing boundary decomposes into finitely many cyclic edge-list contributions.
proof idea
Definition by recursion on the list. The empty case is the zero free chain. The cons case scales singularEdgeListChain of the head term's edges by the head coefficient and adds the recursive value on the tail. No lemmas are invoked; it is pure structural recursion matching the shape of singularEdgeListChain itself.
why it matters
This is the concrete assembly map for the generation half of the circle homology comparison: every balanced free edge-flow should equal such a list sum. Downstream, freeBoundaryKernel_decomposesIntoCyclicEdgeLists is exactly the proposition that zero-boundary free chains are in the image of this map. Support-cardinality induction (freeBoundaryKernel_decomposesIntoCyclicEdgeLists_of_extractionStep), the support-one base (singleEdgeFlow_decomposesIntoCyclicEdgeLists), loop-edge peeling, and singleton-support cases all target equality with this sum.
It also bridges the concrete edge-list interface to the abstract directed-cycle interface via directedCycleListChain_of_cyclicEdgeList, and the singleton identity cyclicSingularEdgeListTermListChain_single ties it to a single term's chain. In the module's program, this is scaffolding for surjectivity of the integer comparison map on $H_1(S^1)$, complementing the already-proved winding-kills-boundaries injectivity half. No Recognition forcing-chain step (T0–T8) is directly at stake; the landmark is the classical $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.