mathlibCircleLinkingBackend_of_cyclicEdgeLists_of_zeroWinding_bounds
plain-language theorem explainer
From two geometric obligations—cyclic edge-list decomposition of balanced free edge-flows, and filling of zero-winding cycles—one obtains a nonempty Mathlib circle-linking backend. Anyone wiring the strict T8 replacement (three spatial dimensions via circle cohomology) cites this packaging step. The proof is a one-line composition: build the integer H₁ isomorphism from those obligations, then hand it to the backend constructor.
Claim. Assume every balanced free singular edge-flow on $S^1$ decomposes into finitely many cyclic edge-list pieces, and every zero-winding singular $1$-cycle is a singular $2$-boundary. Then there exists a Mathlib circle-linking backend: the cohomology-bridge data that supplies the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ used by the strict dimensional forcing.
background
The ambient module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$. Displacement of a singular $1$-simplex is $2\pi$ times winding after reparameterising $\Delta^1$ to the unit interval. 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 fact that the once-around generator has winding $1$, this yields a left inverse to the fundamental class—the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity (generation) needs a filling theorem for zero-winding cycles and a finite cyclic decomposition of balanced free edge-flows.
Those two remaining obligations are packaged as named propositions: freeBoundaryKernel_decomposesIntoCyclicEdgeLists (every balanced free $1$-chain is a finite sum of cyclic edge-list terms) and zeroWindingCycles_bound (every zero-winding $1$-cycle is a $2$-boundary). The Mathlib circle-linking backend is the bridge object that consumes a completed integer $H_1$ isomorphism.
proof idea
One-line term proof. First apply circleH1ZIsoInt_of_cyclicEdgeLists_of_zeroWinding_bounds to the two hypotheses; that lemma reduces the cyclic decomposition to integrality of cycle winding, then feeds integrality plus the zero-winding filling bound into the integral-winding closure to obtain circleH1ZIsoInt. Second, pass that isomorphism to mathlibCircleLinkingBackend_of_circleH1ZIsoInt, which packages a completed integer $H_1$ comparison as a nonempty MathlibCircleLinkingBackend. No extra algebraic work occurs at this layer.
why it matters
Doc-comment places this at the strict T8 replacement: the Recognition forcing chain needs a Mathlib-native circle-linking backend so that $D=3$ spatial dimensions can be read off cohomology rather than a project-local $S^1$ model. The module already closed the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ axiom-free via the winding invariant; this theorem is the packaging gate that turns the two remaining concrete geometric obligations into the backend object the bridge expects.
No downstream consumers are recorded yet (used_by is empty), so the declaration is a terminal assembly point inside CircleWindingChain. The adjacent module comment notes that the finite-flow half can be discharged unconditionally, leaving only the zero-winding filling bound as the live geometric debt. Closing that bound (via subdivision/prism machinery) would fully unlock the Mathlib-backed T8 path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.