zeroWindingCycles_bound_of_orientedCyclicFamilies
plain-language theorem explainer
If every concrete oriented closed walk on S¹ is homologous to an integer multiple of the fundamental cycle, then every singular 1-cycle of winding zero is a 2-boundary. Anyone chasing the generation half of H₁(S¹;ℤ) ≅ ℤ cites this reduction. The proof is a two-step term composition through the global chain-level generation theorem.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If every concrete oriented cyclic family $T$ admits $n\in\mathbb{Z}$ and a singular $2$-chain $b$ with $T\equiv n\cdot\gamma+\partial b$ (where $\gamma$ is the fundamental cycle), then every singular $1$-cycle $z$ with winding $W(z)=0$ is a boundary: $z=\partial b'$ for some singular $2$-chain $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 $F$, the alternating face sum of displacements vanishes. Combined with the fact that the once-around loop has winding $1$, this yields a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. The remaining half is generation: every $1$-cycle is homologous to an integer multiple of the fundamental cycle $\gamma$.
Two concrete geometric targets package that work. The local target orientedCyclicFamilies_boundary_generate asks that each concrete oriented closed walk equal $n\cdot\gamma+\partial b$. The filling target zeroWindingCycles_bound asks that every $1$-cycle of winding zero be a pure $2$-boundary. Upstream, filling the local families already implies global generation (fundamentalCycle_boundary_generates_of_orientedCyclicFamilies), and global generation implies zero-winding filling by writing $z=\partial b+n\gamma$, using that winding kills $\partial b$ and sends $\gamma$ to $1$.
proof idea
One-line term wrapper. Apply fundamentalCycle_boundary_generates_of_orientedCyclicFamilies to the hypothesis to obtain global chain-level generation, then feed that into zeroWindingCycles_bound_of_fundamentalCycle_boundary_generates, which extracts $z=\partial b+n\gamma$, forces $n=0$ from $W(z)=0$, and concludes $z$ is a boundary.
why it matters
Pins the remaining geometric work for the surjectivity half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ to a single local closed-walk filling statement. Downstream, it is one direction of the equivalence orientedCyclicFamilies_boundary_generate_iff_zeroWindingCycles_bound, which "pins the remaining geometric work to one concrete closed-walk filling theorem without changing the final $H_1$ statement." It is also the bridge used by zeroWindingCycles_bound_of_rawPrism, so any raw-prism construction on oriented families immediately closes zero-winding filling. In the Recognition foundation stack this is pure singular-homology infrastructure for the circle, not a T0–T8 forcing step, but it supplies the chain-level generation needed before winding can serve as a complete homology invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.