orientedCyclicFamilies_boundary_generate_of_zeroWindingCycles_bound
plain-language theorem explainer
Zero-winding filling of singular 1-cycles on the circle implies every oriented closed walk is homologous to an integer multiple of the fundamental cycle. Anyone assembling the generation half of H₁(S¹;ℤ) ≅ ℤ cites this implication. The proof is a one-line wrapper that applies the packaged-family method to the filling hypothesis.
Claim. Assume every singular $1$-cycle $z$ on $S^1$ with winding number zero is the boundary of some singular $2$-chain. Then for every oriented cyclic family $T$, there exist an integer $n$ and a $2$-chain $b$ such that the directed cycle of $T$ equals $\partial b + n\,[S^1]$, i.e. $T$ is homologous to an integer multiple of the fundamental cycle.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves the kills-boundaries identity: the alternating face sum of displacements on any singular $2$-simplex vanishes. Combined with the fact that the once-around loop has winding $1$, this yields a left inverse to the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The remaining generation half needs a concrete geometric target. The local target orientedCyclicFamilies_boundary_generate asks that every packaged oriented closed walk be homologous to an integer multiple of the fundamental cycle. The filling hypothesis zeroWindingCycles_bound asks that every zero-winding singular $1$-cycle be a singular $2$-boundary; the module doc notes this is the piece subdivision or prism machinery should supply.
Upstream, the two Props are already defined as the local geometric target and the second concrete geometric subtarget respectively. This theorem is the one-direction bridge from filling to oriented-family generation.
proof idea
One-line term-mode wrapper. Introduce an arbitrary oriented cyclic family term $T$, then apply the method boundary_generate_of_zeroWindingCycles_bound already attached to that packaged term, feeding it the global filling hypothesis. No new chain algebra is performed here; the work lives on the term structure.
why it matters
Closes one arrow of the equivalence between the oriented-family local target and zero-winding filling. Downstream, orientedCyclicFamilies_boundary_generate_iff_zeroWindingCycles_bound uses it as the reverse constructor, and the doc there states the point: "pins the remaining geometric work to one concrete closed-walk filling theorem without changing the final $H_1$ statement." The sibling orientedCyclicFamilies_explicitRawPrism_generate_of_zeroWindingCycles_bound composes this arrow with the raw-prism reduction, so zero-winding filling also yields the fully explicit prism target.
In the broader Recognition foundation this is scaffolding for the surjectivity half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, which underwrites the winding homomorphism used in circle-based forcing arguments. It does not itself touch T5–T8, but it is part of the singular-homology infrastructure those chain steps rely on when they quote circle topology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.