circleH1ZIsoInt_of_largeSupport_of_zeroWinding_bounds
plain-language theorem explainer
From the large-support cyclic edge-list extraction hypothesis and the zero-winding filling bound, the Mathlib bridge isomorphism identifying integer singular homology of the circle with $\mathbb{Z}$ follows. Anyone wiring the circle-linking backend for the strict T8 replacement cites this closure. The proof is a one-line term wrapper: push the large-support step through free-boundary kernel decomposition, then apply the cyclic-edge-list $H_1$ theorem.
Claim. Assume every balanced nonzero free singular $1$-chain with edge-support cardinality greater than one splits as a cyclic edge-list term plus a balanced residual of strictly smaller support, and assume every zero-winding singular $1$-cycle on $S^1$ 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 displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes, by convexity of $\Delta^2$ plus homotopy invariance and additivity of path displacement. Together with the fact that the fundamental loop has winding $1$, this gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Two concrete obligations remain for full Mathlib closure. The large-support extraction step asserts that any balanced nonzero free $1$-chain with edge-support cardinality $>1$ factors as one cyclic edge-list piece plus a balanced residual of strictly smaller support (zero, singleton, and loop-edge branches already closed). The zero-winding bound asserts every singular $1$-cycle of winding $0$ is a singular $2$-boundary.
Upstream, the large-support step alone yields the full free-boundary-kernel cyclic edge-list decomposition; that decomposition plus the zero-winding bound already produce the integer $H_1$ isomorphism.
proof idea
One-line term wrapper. Apply the upstream lemma that turns the large-support extraction hypothesis into the full free-boundary-kernel cyclic edge-list decomposition, then feed that decomposition together with the zero-winding filling hypothesis into the already-proved cyclic-edge-list $H_1$ closure theorem. No new geometric work occurs at this node.
why it matters
This is the final packaging of Mathlib $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ under exactly the two remaining finite-flow and filling targets named in the doc-comment. Downstream it discharges the nonzero $H_1$ backend target and, more importantly, builds the Mathlib circle-linking backend required by the strict T8 replacement (the forcing step that pins spatial dimension $D=3$).
In the Recognition chain, T8 needs a clean integer comparison map on circle homology; the winding homomorphism supplies the left inverse, while cyclic decomposition plus zero-winding filling supply generation. Closing those two props here is what lets the linking backend stand without project-local $S^1$ replacements or axioms. The open geometric work sits inside the two hypotheses themselves (repeated-vertex extraction; prism/subdivision filling), not in this wrapper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.