mathlibCircleLinkingBackend_of_windingHomologyMap_mono
plain-language theorem explainer
Injectivity of the winding map on first singular homology of the circle is enough to assemble the Mathlib circle-linking backend used by the strict T8 replacement. Anyone wiring singular H₁(S¹;ℤ) into dimension forcing or linking would cite this. The proof is a one-line composition: mono of the winding homology map yields the integer isomorphism, which builds the backend.
Claim. If the homology-level winding map $H_1(S^1;\mathbb{Z})\to\mathbb{R}$ is a monomorphism, then there exists a Mathlib circle-linking backend (nonvanishing of Mathlib $H_1(S^1;\mathbb{Z})$ together with the linking-from-circle-$H_1$ interface required by the strict $T_8$ replacement).
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. Combined with the fact that the once-around generator has winding $1$, winding descends to a homology map
$$\mathrm{windingHomologyMap}:H_1(S^1;\mathbb{Z})\to\mathbb{R}.$$
Upstream, mono of that map plus the finite-flow / zero-winding bounds theorem produces circleH1ZIsoInt, i.e. the strong comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The Mathlib circle-linking backend is the structure that packages singular-homology API availability, nonvanishing of that $H_1$, and a linking map routed through the Mathlib circle homology object; it is the concrete replacement target for the old project-local $S^1$ cohomology encoding used in dimension forcing.
proof idea
One-line term wrapper. Apply circleH1ZIsoInt_of_windingHomologyMap_mono to the mono hypothesis to obtain the integer isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Feed that isomorphism into mathlibCircleLinkingBackend_of_circleH1ZIsoInt, which reduces nonemptiness of the backend to nonvanishing of Mathlib circle $H_1$ and packages the linking interface. No new algebraic work occurs at this layer.
why it matters
Closes the last mono-hypothesis gate between the winding-chain computation and the Mathlib-native circle-linking backend demanded by the strict T8 replacement (forcing $D=3$ spatial dimensions via linking/cohomology rather than a bespoke $S^1$ encoding). The doc-comment states exactly that: injectivity of the homology-level winding map is enough to build that backend. Downstream used_by is presently empty in the graph, so this is a terminal assembly lemma in the CircleWindingChain → MathlibCohomologyBridge path; it sits above the finite cyclic edge-list decomposition and zero-winding filling obligations named in the module's final closure comment. Framework landmark: T8 in the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.