closedSingularOneCycleList
plain-language theorem explainer
Finite lists of closed singular 1-simplex generators on S¹ are summed into a single degree-1 cycle in the integer singular chain complex. Anyone proving generation, spanning, or bounding statements for H₁(S¹;ℤ) cites this as the packaging map from closed-edge terms to cycles. The body is a recursive list fold: empty list to zero, cons cell adds the term cycle.
Claim. Given a finite list of closed-generator terms (each a singular $1$-simplex $f:\Delta^1\to S^1$ with equal faces, hence a loop, together with an integer coefficient), form the corresponding degree-$1$ cycle in the singular chain complex of $S^1$ with coefficients in $\mathbb{Z}$ by summing the individual term cycles. The empty list yields the zero cycle.
background
The module lifts the path-level winding and displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$, and proves the chain-level identity that winding kills boundaries. That identity, with the fact that the once-around generator has winding $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A closed-generator term packages one singular $1$-simplex whose two faces coincide (so the simplex is a closed loop) together with an integer coefficient; its associated cycle is the corresponding coproduct summand in $C_1$. The ambient complex is Mathlib's singular chain complex of $S^1$ with integer coefficients: the exact chain-level object whose degree-$1$ homology is the strict comparison target in this foundation layer.
The list map is the finite-sum extension of the single-term cycle constructor, so every later spanning or residual argument can work with ordinary finite lists rather than abstract cycle objects.
proof idea
Definition by recursion on the list. The empty list is sent to the zero cycle. A cons cell adds the cycle of the head term (the integer multiple of the corresponding singular $1$-simplex summand) to the recursive value on the tail. No lemmas are invoked; the body is pure structural recursion into the additive structure of the cycle module.
why it matters
This is the finite-sum packaging used throughout the generation half of the circle homology comparison. Downstream, it feeds the residual-bound generation theorem (zero-winding residual bounds implies the list is a multiple of the fundamental cycle plus a boundary), the conditional generation theorem under the zero-winding-cycles-bound hypothesis, the cone-sum bounding theorem for all-zero-winding lists, the $iCycles$ compatibility with the raw chain list, the spanning proposition for cycle objects, and the winding-integral and zero-winding-residual constructions.
In the module narrative, the missing half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is surjectivity of the integer comparison map: every $1$-cycle homologous to an integer multiple of the fundamental cycle. Finite closed-generator spanning, stated in terms of this list map, is the combinatorial statement left for that generation argument. The upstream complex is flagged as the chain-level object whose degree-$1$ homology is the strict T8-adjacent target in the foundation stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.