mathlibCircleLinkingBackend_of_zeroWinding_bounds
plain-language theorem explainer
Under the sole remaining geometric hypothesis that every zero-winding singular 1-cycle on S¹ is a 2-boundary, the Mathlib circle-linking backend is inhabited. Anyone wiring the strict T8 dimension replacement through Mathlib singular homology cites this. The proof is a one-line term composition: close H₁(S¹;ℤ)≅ℤ from the filling bound, then feed that iso into the backend constructor.
Claim. Assume every singular $1$-cycle $z$ on $S^1$ with winding number zero is the image of some singular $2$-chain under the boundary map. Then the Mathlib circle-linking backend (the cohomology-bridge package required for the strict dimension argument) is nonempty.
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 chain-level fact 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 once-around generator mapping to $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The remaining geometric input is the filling theorem zeroWindingCycles_bound: every singular $1$-cycle of winding zero is a singular $2$-boundary. The finite-flow / integral-winding half has already been discharged unconditionally. The Mathlib circle-linking backend is the packaged interface that the cohomology bridge needs once that $H_1$ comparison iso is in hand.
proof idea
One-line term wrapper. Apply circleH1ZIsoInt_of_zeroWinding_bounds to the hypothesis hzero to obtain the Mathlib $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ package (itself built from the unconditional integral-winding theorem plus the zero-winding filling bound). Pass that package to mathlibCircleLinkingBackend_of_circleH1ZIsoInt, which constructs a witness of MathlibCircleLinkingBackend. No extra tactics or case splits.
why it matters
This is the last conditional gate before the backend is unconditional. Downstream, mathlibCircleLinkingBackend_holds instantiates the theorem at the proved filling bound zeroWindingCycles_bound_holds and asserts that the Mathlib circle-linking backend exists with no remaining hypotheses, "as required by the strict T8 dimension replacement."
In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions. The strict replacement route goes through Mathlib singular homology of the circle rather than a project-local $S^1$ model; the linking backend is the interface that route demands. The module itself uses no axioms, sorry, or local sphere replacements. The only geometric debt this declaration still carries is the named filling hypothesis, which the parent theorem discharges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.