closedSingularOneChainList
plain-language theorem explainer
Sums a finite list of closed singular 1-simplex generators (each with an integer coefficient) into a single degree-1 singular chain on S¹. Anyone working the free-module or cycle-spanning half of H₁(S¹;ℤ) ≅ ℤ cites this as the raw C₁ representative of a closed-generator decomposition. The body is a recursive list fold: empty list to zero, cons adds the term's chain.
Claim. Given a finite list of closed-generator terms (each a singular $1$-simplex on $S^1$ with equal faces and an integer coefficient), form the corresponding element of $C_1(S^1;\mathbb{Z})$ by summing the raw singular chains of the terms. The empty list maps to $0$; a cons cell adds the head term's chain to the sum of the tail.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact needed for a homology invariant. The target complex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients: its $H_1$ is the strict T8 comparison target.
A closed-generator term packages one singular $1$-simplex whose two faces agree (so the simplex is a closed loop), together with an integer coefficient. Each such term has an underlying raw chain in $C_1$ and a cycle representative in the cycles submodule. This definition forgets the cycle packaging and retains only the finite $C_1$ sum.
The surrounding development aims at the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via winding, with the generation/surjectivity half still needing a simplicial prism or subdivision operator Mathlib does not yet supply.
proof idea
Pure recursive definition on lists, no tactics. The empty list is the zero chain in degree $1$. On a cons cell, add the head term's raw chain (the coefficient times the corresponding coproduct summand generator) to the recursively computed sum of the tail. Noncomputable only because the ambient singular chain complex and module structures are.
why it matters
This is the raw $C_1$ evaluation map for finite closed-generator decompositions. Downstream, closedSingularOneCycleList_iCycles proves that including a finite closed-generator cycle list into $C_1$ recovers exactly this sum, and closedSingularOneChainList_spansCycles states that every $1$-cycle, after inclusion into $C_1$, equals such a finite raw sum. The free-module form freeBoundaryKernel_decomposes likewise asks every free edge chain with vanishing free boundary to equal the image of this list sum.
Those spanning statements are the finite-support cancellation half of identifying $H_1(S^1;\mathbb{Z})$ with $\mathbb{Z}$, which the module frames as the remaining generation step toward the strict T8 target (three spatial dimensions via the circle's first homology). Without a concrete $C_1$ fold, the cycle-list and free-kernel props have nothing to equate against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.