closedSingularOneChainList_spansCycles
plain-language theorem explainer
Every integer 1-cycle on the circle, after inclusion into singular C₁, equals a finite raw sum of closed singular edge generators. Anyone proving the generation half of H₁(S¹;ℤ) ≅ ℤ via free-boundary cancellation cites this Prop. It is a named spanning statement, not a proved theorem; later lemmas discharge it from free-boundary kernel decomposition and pass it to cycle-object spanning.
Claim. The property that every degree-$1$ cycle $z$ in the singular chain complex of $S^1$ with integer coefficients has, after inclusion into $C_1$, a representative equal to a finite list-sum of closed singular one-cycle generator terms.
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a finite-support cancellation / spanning statement that Mathlib's singular homology does not yet supply via prism operators.
Here sphereOneSingularIntChainComplex is Mathlib's singular chain complex of TopCat.sphere 1 with $\mathbb{Z}$ coefficients. Cycles in degree $1$ include into $C_1$ via iCycles. A ClosedSingularOneCycleTerm is a closed singular edge generator; closedSingularOneChainList folds a finite list of such terms into an element of $C_1$ by summing their chains.
The Prop records raw-chain spanning: after inclusion, every cycle is exactly such a finite list-sum. The module doc notes this is closer to the actual free-module cancellation theorem than the cycle-object version of the same claim.
proof idea
No proof: the declaration is a def of a Prop. The body is the universal quantifier over degree-$1$ cycles $z$, asserting existence of a list ts of closed singular generator terms such that the image of $z$ under the cycle inclusion equals closedSingularOneChainList ts. Discharge is deferred to the implication from freeBoundaryKernel_decomposes.
why it matters
This Prop is the raw-chain form of closed-generator spanning on $C_1(S^1;\mathbb{Z})$. Downstream, closedSingularOneChainList_spansCycles_of_freeBoundaryKernel_decomposes proves it from free-boundary kernel decomposition in explicit free-module coordinates, and closedSingularOneCycleList_spans_of_chainList_spansCycles lifts it to cycle-object spanning because cycle inclusion is mono.
Together those steps feed the generation half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: every $1$-cycle is homologous to an integer multiple of the fundamental once-around class. That isomorphism is the chain-level target tied to the circle's winding invariant in this foundation layer (the module's "kills-boundaries" identity plus path winding of the fundamental loop already give the split-injective half). It does not itself invoke T5–T8 forcing, but it is infrastructure for the strict $H_1$ computation the foundation stack aims at.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.