directedCycleFreeTermListChain
plain-language theorem explainer
Recursive sum that turns a finite list of directed cycle pieces into one free singular 1-chain on S¹ by adding the chain field of each piece. Anyone citing the free-boundary-kernel cycle decomposition or comparing abstract cycle objects to explicit free chains uses this map. The body is a plain list fold: empty list to zero, cons adds the head chain and recurses.
Claim. Define a map from finite lists of directed cycle pieces to the free $\mathbb{Z}$-module on singular $1$-simplices of $S^1$ by sending the empty list to $0$ and $t::ts$ to $\mathrm{chain}(t)$ plus the image of the tail. Each piece already carries its free $1$-chain representative.
background
The module lifts path 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}$. Generation of the free boundary kernel by directed cycles is the remaining structural input for the integer comparison map.
A directed cycle piece packages an integral $1$-cycle on the singular complex of $S^1$, a free singular $1$-chain, a witness that the free image of the cycle equals that chain, and integrality of the cycle winding. The free module singularOneChainFree is the free $\mathbb{Z}$-module on actual singular $1$-simplices of $\mathrm{TopCat.sphere},1$.
This definition is the list-level summation of those free chains, the explicit side of the correspondence between lists of cycle objects and free edge-chains in the kernel of the free boundary.
proof idea
Definition by structural recursion on the list: the empty list maps to the zero free chain; a cons cell adds the head piece's free chain field to the recursively computed sum of the tail. No lemmas are invoked; noncomputable only because the ambient free-module type is.
why it matters
This is the summation map named in the target of the free-boundary-kernel decomposition: every free edge-chain with vanishing free boundary equals the image of some finite list of directed cycle pieces. The unconditional theorem that discharges that Prop proceeds by $\ell^1$ induction and directed-cycle extraction, and quotes this sum as the reconstructed chain.
Downstream, the equality theorem relating the free image of the listed cycle objects to this sum, the comparison that mapping cyclic edge-list terms to directed-cycle terms preserves free-chain sums, and the oriented-cyclic-family list chain (defined by mapping then summing here) all sit on top of it. In the broader CircleWindingChain program it is bookkeeping infrastructure for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, complementary to the winding-kills-boundaries identity already proved at the simplex level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.