mathlibCircleLinkingBackend_of_largeSupport_of_zeroWinding_bounds
plain-language theorem explainer
Under the large-support cyclic edge-list extraction hypothesis and the zero-winding filling bound, the Mathlib circle-linking backend is inhabited. Anyone wiring the strict T8 replacement through Mathlib singular homology would cite this. The proof is a one-line term composition: feed the conditional H₁(S¹;ℤ) ≅ ℤ package into the backend constructor.
Claim. Assume every balanced nonzero free singular $1$-chain on $S^1$ 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 cycle is a boundary. Then the Mathlib circle-linking backend type is nonempty.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices. The displacement of a singular $1$-simplex is the path displacement of its reparameterization to the unit interval; the key identity is that alternating face sums of displacements vanish on every singular $2$-simplex (winding kills boundaries). Together with the fact that the once-around generator has winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a finite-flow decomposition of free boundary kernels into cyclic edge lists, plus a filling theorem for zero-winding cycles. The remaining finite-flow target after zero/singleton/loop-edge branches is largeSupportCyclicEdgeListExtractionStep: support cardinality $>1$ splits off one cyclic piece with strictly smaller residual support. The companion hypothesis zeroWindingCycles_bound asserts zero-winding cycles bound.
Upstream, circleH1ZIsoInt_of_largeSupport_of_zeroWinding_bounds packages those two inputs into Mathlib's integer comparison isomorphism for circle homology.
proof idea
One-line term wrapper. Apply circleH1ZIsoInt_of_largeSupport_of_zeroWinding_bounds to the two hypotheses to obtain the Mathlib $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ package, then pass that package to MathlibCohomologyBridge.mathlibCircleLinkingBackend_of_circleH1ZIsoInt, which builds a witness of MathlibCircleLinkingBackend. No extra algebraic work occurs at this layer.
why it matters
Doc-comment states the claim directly: the exact two remaining targets build the Mathlib circle-linking backend required by the strict T8 replacement. T8 in the forcing chain forces $D=3$ spatial dimensions; the circle homology computation is the topological backbone that makes the octave/winding story land in Mathlib rather than a project-local $S^1$.
The module already closes the kills-boundaries identity and the winding-on-generator half unconditionally. This theorem is the conditional glue that turns the last finite-flow extraction step plus zero-winding filling into a nonempty linking backend. Downstream use count is currently zero in the graph, so it sits as a terminal assembly point for the Phase-5 Mathlib bridge rather than an intermediate lemma. Nearby module text notes that both oriented-cyclic correction halves are now unconditional, which is the path toward discharging the two hypotheses and obtaining an unconditional backend.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.