zeroWindingCycles_bound_of_explicitRawPrism
plain-language theorem explainer
Fully explicit raw prism fillings for oriented cyclic families on S¹ imply every zero-winding singular 1-cycle is a 2-boundary. Anyone closing the generation half of H₁(S¹;ℤ) ≅ ℤ via prism or subdivision machinery cites this bridge. The proof is a one-line wrapper: package the explicit hypothesis into the raw-prism target, then apply the raw-prism filling theorem.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If every oriented cyclic family admits an explicit raw singular $2$-chain whose boundary equals the raw oriented edge sum minus the matching fundamental-cycle multiple, then every singular $1$-cycle of winding zero is a singular $2$-boundary.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$, and proves that winding kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. Together with the fact that the once-around generator has winding $1$, that yields a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. The converse (every $1$-cycle is homologous to an integer multiple of the fundamental cycle) needs a filling theorem.
The target zeroWindingCycles_bound states exactly that filling: every singular $1$-cycle of winding zero is a $2$-boundary. The hypothesis orientedCyclicFamilies_explicitRawPrism_generate is the fully explicit raw-chain form of the remaining prism obligation: for each concrete oriented cyclic family term $T$, produce an integer $n$ and a singular $2$-chain $b$ with $\partial b$ equal to the raw oriented edge sum of $T$ minus $n$ times the fundamental cycle.
Upstream, the packaged raw-prism target is implied by the explicit one, and the raw-prism target already closes zero-winding filling via the oriented-cyclic-family boundary generator.
proof idea
One-line term-mode wrapper. First apply orientedCyclicFamilies_rawPrism_generate_of_explicit to the given explicit-raw-prism hypothesis, obtaining the packaged raw-prism generation property. Then feed that into zeroWindingCycles_bound_of_rawPrism, which (under the same decidable-equality instances) already reduces raw-prism generation to zero-winding filling via the oriented-cyclic-family boundary generator. No new geometric construction occurs here.
why it matters
This sits in the generation half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: the split-injective half is already settled by winding-kills-boundaries plus the fundamental loop; surjectivity needs every zero-winding cycle to bound. The theorem converts a fully explicit raw-prism construction into that filling target.
Downstream it is one direction of the equivalence between the explicit raw-prism target and zero-winding filling, and it is the bridge used by the free-coordinate prism variant (zeroWindingCycles_bound_of_freePrism), which packages free prisms into explicit raw prisms and then applies this result. In the broader Recognition foundation stack this is scaffolding toward a complete singular-homology computation of the circle without project-local $S^1$ replacements, feeding any later argument that needs the fundamental class to generate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.