orientedCyclicFamilies_explicitRawPrism_generate_of_zeroWindingCycles_bound
plain-language theorem explainer
Zero-winding filling of singular 1-cycles on the circle yields the fully explicit raw-prism generation target for oriented cyclic families. Cite this when reducing prism/subdivision generation of H₁(S¹) to a geometric filling hypothesis. The proof is a pure composition: zero-winding bound implies local boundary generation, which then upgrades to the explicit raw-chain prism equality.
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 singular $2$-chain $b$ such that $\partial b$ equals the raw oriented edge-sum of $T$ minus $n$ times the fundamental cycle.
background
This module lifts path-level winding on the circle to singular simplices of $S^1$ 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$, that gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation (surjectivity) half needs a prism or subdivision construction that Mathlib singular homology does not yet supply.
The hypothesis zeroWindingCycles_bound is the concrete geometric subtarget: every zero-winding singular $1$-cycle is a singular $2$-boundary. The conclusion orientedCyclicFamilies_explicitRawPrism_generate asks, for each oriented cyclic family term $T$, for an integer $n$ and a raw $2$-chain $b$ with $\partial b$ equal to the free oriented edge sum of $T$ minus $n$ times the fundamental cycle. An intermediate target packages the same demand at the level of cycle objects (boundary generation for oriented families).
proof idea
Pure term-mode composition of two already-proved implications. First apply the lemma that zero-winding filling implies oriented-family boundary generation (it feeds the packaged cycle of each family into the global fundamental-cycle generation theorem). Then apply the lemma that boundary generation upgrades to the fully explicit raw-chain prism equality (extract $n$ and $b$ from the raw-prism transport of the cycle-object witness). No new geometry is proved here.
why it matters
Closes one direction of the equivalence between the fully explicit raw-prism target and zero-winding filling, and thereby feeds the three Phase-5 checklist equivalences: explicit-raw, free-coordinate, and packaged-raw prism generation are each equivalent to the geometric filling theorem. Downstream docs state the point bluntly: "the only remaining gap is the geometric filling construction itself." In the module's larger program this is the generation half of the integer comparison map on $H_1(S^1)$, complementary to the already-proved kills-boundaries identity and the winding of the fundamental loop. No Recognition forcing-chain step (T0–T8) is discharged here; the lemma is pure singular-homology scaffolding for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.