orientedCyclicFamilies_boundary_generate_iff_zeroWindingCycles_bound
plain-language theorem explainer
The local oriented-family generation target on singular 1-cycles of S¹ is equivalent to the zero-winding filling statement: every winding-zero cycle is a 2-boundary. Anyone reducing the generation half of H₁(S¹;ℤ) ≅ ℤ to a single geometric filling theorem will cite this. The proof is a two-line constructor applying the two already-proved implication lemmas.
Claim. The following are equivalent: (i) every oriented cyclic family term is homologous to an integer multiple of the fundamental cycle of $S^1$; (ii) every singular $1$-cycle $z$ on $S^1$ with winding number zero is the boundary of some singular $2$-chain.
background
This module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$. The displacement of a singular $1$-simplex is $2\pi$ times winding, obtained by reparameterizing $\Delta^1$ to the unit interval. The key identity is that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes, by convexity of $\Delta^2$ and homotopy invariance of path displacement.
Two concrete geometric Props package the remaining generation work. The oriented-family target asserts that every concrete oriented closed walk, packaged as an OrientedCyclicFamilyTerm, is homologous to an integer multiple of the fundamental cycle. The zero-winding filling target asserts that every singular $1$-cycle of winding zero is a singular $2$-boundary. Both sit inside the integer singular chain complex of $S^1$.
Together with the fact that winding sends the once-around generator to $1$, these targets supply the generation half of the comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The split-injective half is already available from the kills-boundaries identity.
proof idea
Classical constructor on the biconditional. Forward direction: feed the oriented-family hypothesis into zeroWindingCycles_bound_of_orientedCyclicFamilies, which routes through fundamental-cycle generation and then specializes to zero-winding cycles. Reverse direction: apply orientedCyclicFamilies_boundary_generate_of_zeroWindingCycles_bound, which packages each oriented family as a cycle and invokes the global zero-winding filler. No new geometry is proved here; the two one-way lemmas are simply glued.
why it matters
Pins the remaining geometric obligation for the surjectivity half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ to a single closed statement: zero-winding cycles bound. The module doc states that Mathlib's singular homology does not yet supply the prism/subdivision operator needed for that filling; this equivalence lets later work target either the oriented-walk form or the zero-winding form without changing the final $H_1$ claim.
In the Recognition Science foundation stack, a clean integer comparison for circle homology underwrites the eight-tick octave and the winding bookkeeping used in the forcing chain. No downstream consumers are wired yet (used_by is empty), so this is a consolidation lemma inside CircleWindingChain rather than a leaf of a larger proved theorem. It closes no sorry; it only identifies two already-named geometric Props.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.