circleH1ZIsoInt_of_extractionStep_of_zeroWinding_bounds
plain-language theorem explainer
Assuming a support-decreasing cyclic extraction step on balanced free edge-flows and that every zero-winding singular 1-cycle bounds, the Mathlib bridge yields H₁(S¹;ℤ) ≅ ℤ. Anyone wiring the circle-linking backend for the strict T8 path cites this. The proof is a one-line composition: extraction implies full cyclic edge-list decomposition, then the prior cyclic-lists closure applies.
Claim. If every nonzero balanced free edge-flow splits as a cyclic edge-list summand plus a residual of strictly smaller edge support, and every singular $1$-cycle $z$ on $S^1$ with winding $0$ is a singular $2$-boundary, then the Mathlib cohomology 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 via simplexDisplacement (reparameterize $\Delta^1$ to $[0,1]$ and take path displacement). The key identity is that alternating face sums of displacements vanish on every singular $2$-simplex: winding kills boundaries. Together with the fundamental loop having winding $1$, this gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The remaining generation half is packaged as two concrete obligations. The extraction step says every nonzero balanced free edge-flow factors as one cyclic edge-list piece plus a balanced residual of strictly smaller support. Zero-winding filling says every singular $1$-cycle of winding zero is a $2$-boundary. An upstream theorem already closes the isomorphism once full finite cyclic decomposition and zero-winding filling are granted; another lifts the one-step extraction to that full decomposition by strong induction on support cardinality.
proof idea
One-line term wrapper. Apply the induction theorem that turns the one-step extraction hypothesis into full finite cyclic edge-list decomposition of the free boundary kernel. Feed that decomposition, together with the zero-winding filling hypothesis, into the prior closure theorem that already produces the Mathlib integer $H_1$ isomorphism from those two obligations.
why it matters
This is the final packaging step that turns the two remaining geometric subtargets (support-decreasing cyclic extraction, zero-winding filling) into the Mathlib $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ bridge object. Downstream it immediately yields the nonzero $H_1$ target and, more importantly, a nonempty Mathlib circle-linking backend: that backend is what the strict T8 replacement demands when $D=3$ spatial dimensions are forced through circle linking rather than a project-local $S^1$ stand-in.
In the module's own terms, injectivity of the winding comparison is already settled by the kills-boundaries identity and the fundamental loop; this theorem is the generation/surjectivity half under the two named hypotheses. It does not invent new geometry: it only composes the extraction-to-decomposition induction with the cyclic-lists closure so the linking backend can be assembled in one place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.