mathlibCircleLinkingBackend_of_extractionStep_of_zeroWinding_bounds
plain-language theorem explainer
Assuming a support-decreasing cyclic extraction on free edge-flows and a filling theorem for zero-winding singular 1-cycles, the Mathlib circle-linking backend is inhabited. Anyone wiring the strict T8 replacement through singular homology of S¹ cites this bridge. The proof is a one-line composition: build the integer H₁ isomorphism from the two geometric hypotheses, then hand it to the backend constructor.
Claim. If every nonzero balanced free singular edge-flow decomposes as one cyclic edge-list term plus a residual of strictly smaller edge support, and every singular $1$-cycle on $S^1$ of winding zero is a singular $2$-boundary, then the Mathlib circle-linking backend is nonempty.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices: each $f:C(\Delta^1,S^1)$ gets a real displacement (equivalently $2\pi$ times winding) by reparameterizing $\Delta^1$ to the unit interval. The key identity is that alternating face sums of displacements vanish on every singular $2$-simplex, so winding descends to a homology invariant and supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The two named hypotheses close the remaining generation half. The extraction step says every nonzero balanced free edge-flow splits as a cyclic edge-list piece plus a balanced residual of strictly smaller support. The zero-winding bound says every singular $1$-cycle of winding zero is already a singular $2$-boundary (the filling theorem expected from prism/subdivision machinery).
Upstream, those two props already yield the integer comparison isomorphism on $H_1$; a separate bridge lemma turns any such isomorphism into a Mathlib circle-linking backend.
proof idea
Pure one-line term wrapper. First apply the upstream closure that turns the extraction step and the zero-winding filling bound into the Mathlib integer $H_1$ isomorphism. Then feed that isomorphism to the existing constructor that builds a nonempty Mathlib circle-linking backend from any such iso. No extra algebraic work happens at this layer.
why it matters
The nearby module comment states the point bluntly: these two remaining geometric targets build the Mathlib circle-linking backend required by the strict T8 replacement. In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions; the circle-linking/cohomology bridge is the Mathlib-native route that replaces ad-hoc $S^1$ scaffolding with singular homology.
This declaration packages the last two open geometric props into the exact backend structure the bridge demands. It sits at the end of the CircleWindingChain assembly: winding kills boundaries, cyclic extraction generates free cycles, zero-winding cycles fill, the integer iso closes, and the backend is inhabited. No further used-by edges are recorded yet; the consumer is the strict T8 replacement path itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.