cycleWinding_integral_of_closedSingularOneCycleList_spans
plain-language theorem explainer
If every singular 1-cycle on the circle is a finite sum of closed generator cycles, then every cycle has integer winding. Cited by anyone reducing the integrality half of the H₁(S¹;ℤ) ≅ ℤ comparison to a combinatorial spanning statement. The proof unpacks the spanning witness, applies the list-level integer-winding lemma, and rewrites.
Claim. Assume every singular $1$-cycle $z$ on $S^1$ equals a finite list-sum of closed singular generator cycles. Then for every such $z$ there exists an integer $n$ with $\mathrm{winding}(z)=n$ as a real.
background
This module lifts the path-level winding invariant of the circle to singular $1$-simplices on $S^1$ and proves that winding kills boundaries: the alternating face sum of displacements on any singular $2$-simplex vanishes. Combined with the fact that the once-around generator has winding $1$, that yields a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$).
The remaining generation half needs two geometric subtargets. The first is integrality: every singular $1$-cycle has integer winding. The second is filling: every zero-winding cycle is a singular $2$-boundary.
Here integrality is packaged as a proposition: for every cycle $z$ there is an integer $n$ with $\mathrm{winding}(z)=n$ in $\mathbb{R}$. The spanning hypothesis says every cycle equals a finite list-sum of closed singular generator terms. An upstream lemma already shows any such finite list has integer winding.
proof idea
Short tactic proof. Fix a cycle $z$. From the spanning hypothesis obtain a finite list $ts$ of closed singular generator terms with $z$ equal to that list-sum. Apply the upstream list-integrality theorem to $ts$ to obtain an integer $n$ and the equality of the list-sum winding with $n$. Rewrite along the spanning equality to conclude $\mathrm{winding}(z)=n$.
why it matters
This is the conditional discharge of the first concrete geometric subtarget toward the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the circle-winding chain. The module already has the kills-boundaries identity and the fundamental-loop normalization; what remains is to show every cycle is homologous to an integer multiple of the fundamental cycle. Integrality of winding on all cycles is the first step of that program; the second (zero-winding cycles are boundaries) is left to prism or subdivision machinery.
No downstream consumers are wired yet. The result sits in Foundation as topological scaffolding for discrete circular structure (the eight-tick octave and related period-$2^3$ landmarks later in the forcing chain). It does not itself touch mass ladders, $\alpha$, or the $J$-cost uniqueness theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.