cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoCyclicEdgeLists
plain-language theorem explainer
Assuming every balanced free edge-flow on the circle decomposes into finitely many cyclic edge-list pieces, every singular 1-cycle has integer winding. Anyone closing the integer comparison map H₁(S¹;ℤ) → ℤ cites this bridge. The proof is a one-line composition: cyclic lists imply directed-cycle decomposition, which already yields integer winding.
Claim. If every free singular $1$-chain $c$ with vanishing free boundary decomposes as a finite sum of cyclic edge-list terms, then for every singular $1$-cycle $z$ on $S^1$ there exists $n\in\mathbb{Z}$ such that the winding of $z$ equals $n$ as a real number.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes by convex telescoping inside $\Delta^2$. Combined with the once-around generator mapping to $1$, this supplies a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class (the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$).
The target proposition cycleWinding_integral asserts that every singular $1$-cycle has integer winding, expected from endpoint cancellation in a finite integer chain. Two kernel-decomposition hypotheses sit upstream: the concrete one says every balanced free edge-flow is a finite list of cyclic edge-list terms; the abstract one says the same for directed-cycle pieces. An intermediate theorem already converts the abstract directed-cycle hypothesis into integer winding for all cycles.
proof idea
One-line term-mode wrapper. Apply the lifting theorem that turns a cyclic edge-list kernel decomposition into a directed-cycle kernel decomposition, then feed that hypothesis into the existing theorem that directed-cycle decomposition implies integer winding on every singular $1$-cycle. No new geometric argument appears here; the work is pure hypothesis transport along the already-proved implication chain.
why it matters
This is the concrete-hypothesis entry point for integer winding used by the final Mathlib $H_1$ closure. Downstream, circleH1ZIsoInt_of_cyclicEdgeLists_of_zeroWinding_bounds takes the cyclic edge-list decomposition together with a zero-winding filling bound and produces the integer isomorphism bridge; it invokes exactly this theorem to discharge the integral-winding obligation.
In the module narrative this is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is already a left inverse to the fundamental class once it lands in $\mathbb{Z}$. Surjectivity (generation by the fundamental loop) remains the separate open half and needs simplicial prism or subdivision structure that Mathlib singular homology does not yet supply. No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked; the result is pure foundational topology supporting later circle and ledger constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.