zeroWindingCycles_bound_of_freePrism
plain-language theorem explainer
Assuming free-coordinate prism fillings exist for every oriented cyclic family, every singular 1-cycle on S¹ with vanishing winding is a singular 2-boundary. Cite this when discharging the zero-winding filling half of H₁(S¹;ℤ) ≅ ℤ from a free C₂ prism hypothesis. The proof is a one-line transport: free prisms yield explicit raw prisms, which already close the bound.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If every oriented cyclic family admits a free-coordinate prism (an explicit free $C_2$ chain whose free boundary equals the oriented edge sum minus the free image of the matching fundamental cycle), then every singular integer $1$-cycle $z$ on $S^1$ with cycle winding $0$ is a boundary: there exists a $2$-chain $b$ with $z = \partial b$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. Together with the fact that the once-around loop has winding $1$, this gives a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$. The remaining generation half needs a filling theorem: zero-winding cycles must be boundaries.
That filling target is packaged as zeroWindingCycles_bound: every cycle $z$ in the singular integer chain complex of $S^1$ with cycle winding $0$ is the image of some $2$-chain under the boundary-to-cycles map. The free-coordinate prism hypothesis asks, for each oriented cyclic family $T$, for a free $C_2$ chain $B$ whose free boundary equals the oriented edge sum of $T$ minus the free-coordinate image of the matching fundamental cycle. This is the cleanest hand-built finite prism target in the chain.
Upstream, free prisms transport to fully explicit raw prisms (after pushing the free $C_2$ boundary through Mathlib's raw chain complex), and explicit raw prisms already imply the zero-winding bound.
proof idea
One-line term wrapper. Apply the upstream transport orientedCyclicFamilies_explicitRawPrism_generate_of_freePrism to the free-prism hypothesis, obtaining the explicit raw-prism generation property. Feed that into zeroWindingCycles_bound_of_explicitRawPrism, which already closes the zero-winding filling target (itself via the raw-prism intermediate). No new geometric construction appears here; the work is hypothesis transport along the free-to-explicit-raw prism ladder.
why it matters
This sits on the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding already splits the fundamental class injectively; zero-winding cycles must still be shown to bound. The free-coordinate prism is the cleanest finite $C_2$ target for a hand-built prism, so discharging the bound from that hypothesis is the natural reduction step.
Downstream, zeroWindingCycles_bound_of_pathConeCorrection routes the path-cone residual correction target through free prisms into this theorem, so the whole correction ladder lands on the same filling statement. In the module's terms, this is the subdivision/prism half Mathlib's singular homology does not yet supply; closing any of the prism hypotheses (free, explicit raw, path-cone) finishes the integer comparison map's surjectivity on $S^1$.
Framework-wise this is pure foundation topology supporting later Recognition chain work, not a T0–T8 forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.