orientedCyclicFamilies_rawPrism_generate_iff_zeroWindingCycles_bound
plain-language theorem explainer
The packaged raw-prism generation target for oriented cyclic families on S¹ is equivalent to zero-winding cycle filling. Anyone assembling the generation half of H₁(S¹;ℤ) ≅ ℤ from singular prisms would cite this bridge. Both directions route through the already-proved explicit raw-prism intermediate via a short constructor.
Claim. Assuming decidable equality on singular $0$- and $1$-simplices of $S^1$, the raw-prism generation property for oriented cyclic families is equivalent to the zero-winding cycles filling bound: every oriented cyclic family $T$ admits a singular $2$-chain $b$ and integer $n$ with $\partial b = [T] - n\,[S^1]$ if and only if every zero-winding singular $1$-cycle is a boundary (under the stated bound).
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$. The key chain-level fact is that simplex 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. Together with the fact that the fundamental loop has winding $1$, this yields a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$.
The remaining generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a singular prism or subdivision operator that Mathlib does not yet supply. The raw-prism target packages exactly that geometric obligation: for each oriented cyclic family term $T$, some $2$-chain $b$ has boundary equal to the family's directed cycle minus an integer multiple of the fundamental cycle.
Zero-winding filling is the dual geometric subtarget: cycles of winding zero are boundaries. An explicit (fully expanded edge-sum) form of the raw-prism target is already known equivalent to zero-winding filling; the packaged form is identified with that explicit form by the cycle-object versus signed-edge-sum correspondence.
proof idea
Term-mode constructor on the biconditional.
Forward: from packaged raw-prism generation, apply the identification that turns a packaged witness into an explicit raw-prism witness, then the left-to-right half of the already-proved equivalence between explicit raw-prism generation and zero-winding filling.
Reverse: from zero-winding filling, obtain an explicit raw-prism witness via the right-to-left half of that same equivalence (itself routed through boundary generation), then repackage the explicit witness as a packaged raw-prism witness.
No new geometry is proved here; the argument is pure transport across two prior equivalences.
why it matters
Closes the last packaging gap between the two concrete geometric subtargets named in the module's final H₁-closure comment: integer winding on cycles, and filling of zero-winding cycles. The module doc states that the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is already in hand from the kills-boundaries identity plus winding of the fundamental loop; surjectivity of the integer comparison map is the generation half and is exactly what the prism target encodes.
No downstream consumers are wired yet (used_by is empty), so this sits as a ready interface lemma for the final Mathlib H₁ comparison. In the broader Recognition foundation it is pure singular-homology infrastructure: it does not touch the forcing chain T0–T8, the Recognition Composition Law, or the $\varphi$-ladder, but it supplies the circle's first homology as a clean $\mathbb{Z}$ that later recognition and phase arguments can quote without project-local $S^1$ replacements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.