closedSingularOneChainList_spansCycles_of_freeBoundaryKernel_decomposes
plain-language theorem explainer
If every free singular 1-chain with vanishing free boundary is a finite sum of closed singular edge cycles, then every actual integer 1-cycle on S¹, after inclusion into C₁, equals such a finite raw sum. Anyone closing the generation half of H₁(S¹;ℤ) ≅ ℤ would cite this bridge. The proof maps the cycle into free coordinates, applies the kernel hypothesis, and pulls the equality back by injectivity of the free-chain isomorphism.
Claim. Assume every free singular $1$-chain $c$ with free boundary zero equals a finite list-sum of closed singular edge cycles. Then for every singular $1$-cycle $z$ on $S^1$ with integer coefficients, the image of $z$ under the cycles inclusion $Z_1\hookrightarrow C_1$ equals a finite list-sum of closed singular generators.
background
This module lifts path-level winding on the circle to singular simplices of TopCat.sphere 1 and proves that displacement kills boundaries, giving the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The remaining generation half needs every $1$-cycle to be homologous to an integer multiple of the fundamental loop; the present statements work at the raw finite-support chain level toward that goal.
The free edge module carries an explicit boundary sending each directed singular edge to terminal face minus initial face. The free-boundary kernel decomposition asserts that every free $1$-chain with vanishing free boundary is a finite sum of closed singular edge cycles (edges whose two faces coincide). The raw-chain spanning property asks the same of actual cycle representatives after the cycles inclusion into $C_1$ of the Mathlib singular chain complex of $S^1$ with $\mathbb{Z}$ coefficients.
An isomorphism identifies ordinary singular $1$-chains with the free module on singular $1$-simplices, so kernel statements in free coordinates can be transported to genuine cycles once injectivity is available.
proof idea
Fix a $1$-cycle $z$. Form the free chain $c$ by composing the cycles inclusion with the free-chain isomorphism. Commutation of that isomorphism with boundary, plus the fact that cycles are killed by the differential, yields free boundary of $c$ equal to zero. The hypothesis then supplies a finite list of closed generators whose free image is $c$.
It remains to descend the equality to $C_1$. The free-chain map is an isomorphism (hence mono), so its underlying function is injective; applying injectivity to the free equality recovers the desired raw-chain identity for the included cycle.
why it matters
Generation of $H_1(S^1;\mathbb{Z})$ by the once-around class is the open half of the integer comparison isomorphism; the module doc identifies that isomorphism as the strict chain-level T8 target. This theorem is the pure logical bridge from the free-module cancellation statement to the spanning statement on genuine cycle representatives, which is the form needed by finite-support winding and cone arguments downstream in the same file.
No downstream consumers are wired yet (used_by is empty), so the declaration presently sits as infrastructure: once free-boundary kernel decomposition is discharged, raw-cycle spanning drops out immediately and feeds the list-ready cone and winding-integral lemmas that follow in the module. It does not itself touch the forcing chain T0–T8 landmarks beyond supplying homology infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.