closedSingularOneCycleList_spans
plain-language theorem explainer
Names the finite-support spanning property: every integer singular 1-cycle on S¹ equals the cycle assembled from a finite list of closed singular generator terms. Cited as the combinatorial hypothesis that unlocks integer-valued cycle winding and fundamental-cycle generation. Pure Prop definition; no proof content.
Claim. The proposition that every $1$-cycle $z$ in the integer singular chain complex of $S^1$ equals the cycle obtained from some finite list of closed singular generator terms (each term a closed singular $1$-simplex packaged as a cycle).
background
The module lifts path winding on $S^1$ to singular $1$-simplices via simplexDisplacement (reparameterize $\Delta^1$ to $[0,1]$ and take path displacement) and proves the kills-boundaries identity: the alternating face sum of displacement on any singular $2$-simplex vanishes. That identity makes winding a homology invariant and supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The ambient complex is Mathlib's singular chain complex of TopCat.sphere 1 with coefficients in $\mathbb{Z}$. Degree-$1$ cycles are the objects of interest. A closed singular generator term packages a closed singular $1$-simplex as a cycle; a finite list of such terms is summed (by recursion, empty list to zero) to a single cycle object.
This Prop asserts that those finite closed-generator sums exhaust the full cycle module: every $1$-cycle arises that way. It is the finite-chain combinatorial statement the module leaves open for the integrality and generation arguments.
proof idea
Definitional: the body is the universal quantification over degree-$1$ cycles of the existence of a finite list of closed singular generator terms whose list-sum cycle equals the given cycle. No tactics or lemmas. Downstream, the monomorphism property of the cycle inclusion is used to transfer an analogous raw-chain spanning statement into this cycle-object form.
why it matters
This is the finite-support spanning hypothesis that the module isolates so the remaining work toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ splits cleanly. Assuming it, every cycle has integer winding (via the list winding integrality lemma), and together with zero-winding filling one obtains full fundamental-cycle boundary generation: every cycle is homologous to an integer multiple of the once-around class.
In the Recognition Science chain this supports the strict T8 target (three spatial dimensions via the circle homology computation that anchors the octave and dimensional forcing). The module already has winding kills boundaries and the fundamental loop maps to $1$; what remains is generation/surjectivity of the integer comparison map, which Mathlib's singular homology does not yet supply via prism/subdivision. Naming this Prop separates that combinatorial gap from the analytic filling step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.