closedSingularOneCycleList_winding_integral
plain-language theorem explainer
Any finite list of closed singular 1-generator terms on S¹ has integer total winding. Homology workers cite it when reducing the integer-valuedness of the winding map to the closed-generator span. The proof is list induction: empty list gives 0; the cons case adds the head term's integer winding to the inductive tail.
Claim. For every finite list of closed singular one-cycle terms (each a singular $1$-simplex on $S^1$ with equal endpoints, together with an integer coefficient), the winding number of the associated degree-$1$ cycle is an integer: there exists $n\in\mathbb{Z}$ such that the winding of the summed cycle equals $n$ as a real.
background
The module lifts the path-level winding invariant of the circle to singular simplices of $S^1$ and proves that winding kills boundaries, so it descends to a homology invariant. Concretely, simplexDisplacement reparameterizes $\Delta^1$ to the unit interval and reads off path displacement ($2\pi$ times winding); the alternating face sum on any singular $2$-simplex vanishes by a convex-simplex homotopy and path additivity.
A closed-generator term packages one singular $1$-simplex whose two faces agree (so it is a closed loop on $S^1$) with an integer coefficient; its cycle is the corresponding free-chain element. A finite list of such terms is summed to a genuine $1$-cycle via the recursive list-to-cycle map. Winding of a cycle is the composite of the cycle inclusion into $C_1(S^1;\mathbb{Z})$ with the winding chain map, landing in $\mathbb{R}$.
The global target is that every singular $1$-cycle has integer winding (the integrality half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). This declaration settles that claim on the closed-generator span.
proof idea
Pattern-match on the list. For the empty list, unfold the list-to-cycle map and the winding functional; both sides are zero, so take $n=0$.
For a cons cell $t::ts$, invoke the head term's own integrality fact to obtain an integer $n_1$ with winding of $t$'s cycle equal to $n_1$, and recurse on the tail to obtain $n_2$. Claim $n_1+n_2$. Unfold the list-to-cycle sum and the winding definition; winding is a module homomorphism, so it preserves addition. Rewrite by the two inductive equalities and simplify the integer cast.
why it matters
This is the algebraic integrality step on the closed-generator presentation of cycles. Downstream, the zero-winding residual theorem subtracts the matching integer multiple of the fundamental cycle from any closed-generator list and obtains a residual of winding zero: the algebraic shell around the remaining geometric filling problem. Separately, if every cycle is a finite sum of closed singular generators, the span hypothesis plus this theorem yields full cycle integrality.
In the module's larger program, winding already kills boundaries and sends the once-around generator to $1$, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Integrality on a generating class of cycles is the complementary bookkeeping needed before the generation/surjectivity half (simplicial prisms and subdivision, still outside Mathlib's singular homology). No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the result is pure circle homology infrastructure that later RS geometry can quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.