zeroWindingCycles_bound_iff_windingHomologyMap_mono
plain-language theorem explainer
Chain-level zero-winding filling (every singular 1-cycle of winding 0 is a 2-boundary) is equivalent to injectivity of the induced winding map on H₁(S¹;ℤ). Anyone tracking the split-injective half of H₁(S¹;ℤ) ≅ ℤ via the winding invariant will cite this bridge. The proof is a two-direction constructor that routes each side through the intermediate homology-class vanishing statement.
Claim. The following are equivalent: (i) every singular $1$-cycle $z$ on $S^1$ with cycle winding $0$ is the boundary of some singular $2$-chain; (ii) the induced winding homomorphism $H_1(S^1;\mathbb{Z})\to\mathbb{R}$ is a monomorphism (injective).
background
This module lifts path-level winding on $S^1$ to singular simplices. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval; the key identity is that alternating face displacements of any singular $2$-simplex vanish (winding kills boundaries). That makes winding a chain map on cycles and induces a homology-level map.
The winding homology map is the factorization of the winding chain map through $H_1(S^1;\mathbb{Z})$ into $\mathbb{R}$. The geometric filling target zeroWindingCycles_bound asserts: every $1$-cycle of winding zero is literally a $2$-boundary. An intermediate Prop records that such cycles have vanishing homology class.
Together with the fact that winding sends the once-around generator to $1$, injectivity of the homology map is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Full generation (surjectivity of the integer comparison) still needs prism/subdivision machinery Mathlib does not yet supply.
proof idea
Standard constructor on the biconditional. Forward: assume the filling bound; pass through the lemma that filling implies homology-class vanishing for zero-winding cycles, then apply the mono-from-class-zero theorem to conclude the winding homology map is mono. Reverse: assume mono; pass through the lemma that mono implies homology-class vanishing, then apply the bound-from-class-zero theorem to recover explicit $2$-chain fillings. Both directions are pure composition of already-proved one-way implications; no new geometric work.
why it matters
Closes the logical circle between the concrete geometric filling target and injectivity of the homology-level winding map. In the module's program this is the bridge that lets either formulation stand for the "split-injective" half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ once winding kills boundaries and hits the fundamental loop by $1$. Downstream use is currently empty in the graph, so the declaration is a consolidation lemma rather than a leaf feeder. It does not touch the forcing chain (T0–T8), RCL, or $\varphi$-ladder physics; it is pure singular-homology infrastructure for the circle. The remaining open half of the classical isomorphism (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still depends on subdivision/prism operators not yet in Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.