circleH1ZIsoInt_of_cyclicEdgeLists_of_zeroWinding_bounds
plain-language theorem explainer
From finite cyclic edge-list decomposition of balanced free edge-flows plus filling of zero-winding cycles, one obtains the Mathlib isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Anyone closing the singular-homology comparison for the circle cites this bridge. The proof is a one-line reduction: cyclic decomposition yields integer winding on cycles, then the integral-winding-plus-zero-filling closure applies.
Claim. Assume every balanced free singular edge-flow decomposes into finitely many cyclic edge-list pieces, and every singular $1$-cycle of winding zero is a singular $2$-boundary. Then the Mathlib bridge supplies an isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval. The key identity is that displacement kills boundaries: for any singular $2$-simplex the alternating face sum of displacements vanishes, by convexity of $\Delta^2$ and homotopy invariance of path displacement.
Together with the fact that winding sends the once-around generator to $1$, this gives a left inverse to the fundamental class (injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity needs a generation statement: every $1$-cycle is homologous to an integer multiple of the fundamental cycle.
Two concrete obligations remain. The cyclic edge-list decomposition says every free $1$-chain with vanishing free boundary is a finite sum of cyclic singular edge-list terms. Zero-winding filling says every singular $1$-cycle of winding zero is a $2$-boundary. Upstream, the cyclic decomposition already implies integer winding on all singular $1$-cycles.
proof idea
One-line term wrapper. First apply the upstream lemma that converts cyclic edge-list decomposition of the free boundary kernel into the integer-winding property on cycles. Feed that integer-winding hypothesis, together with the given zero-winding filling bound, into the prior closure theorem that builds the Mathlib $H_1$ isomorphism from integer winding plus zero-winding filling. No extra algebraic work occurs at this layer.
why it matters
This is the final Mathlib $H_1$ closure packaged at the cyclic-edge-list granularity named in the doc-comment. Downstream it is the direct parent of the extraction-step and large-support closures (each reduces its finite-flow hypothesis to cyclic edge-lists, then calls this theorem). It also yields the nonzero $H_1$ target and the Mathlib circle-linking backend required by the strict T8 replacement (three spatial dimensions via circle linking).
In the broader Recognition chain, T8 forces $D=3$; the linking backend is the homology input that makes that dimensional forcing sit on Mathlib singular homology rather than a project-local $S^1$. The remaining open geometric work is discharging the two named hypotheses themselves (support-decreasing cyclic extraction, and prism/subdivision filling of zero-winding cycles).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.