zeroWindingCycles_bound_of_rawPrism
plain-language theorem explainer
If every oriented cyclic family on S¹ admits a raw singular 2-chain prism whose boundary is the closed walk minus an integer multiple of the fundamental cycle, then every singular 1-cycle of winding zero is a 2-boundary. Cited by anyone closing the generation half of H₁(S¹;ℤ) ≅ ℤ via prism fillings. The proof is a two-step term composition through the oriented-family boundary target.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If for every oriented cyclic family $T$ there exist an integer $n$ and a singular $2$-chain $b$ with $\partial b = T^{\mathrm{cyc}} - n\,[S^1]$, then every singular $1$-cycle $z$ with winding number zero is a singular $2$-boundary: $\mathrm{wind}(z)=0$ implies $z=\partial b'$ for some $2$-chain $b'$.
background
The module lifts path-level winding on the circle to singular simplices of TopCat.sphere 1. Displacement of a singular 1-simplex is path displacement after reparameterizing Δ¹ to the unit interval; the key identity is that alternating face sums of any singular 2-simplex have vanishing displacement (winding kills boundaries). Together with the once-around generator mapping to 1, this yields a left inverse to the fundamental class on H₁(S¹;ℤ).
The remaining generation half needs prism/subdivision machinery Mathlib does not yet supply. The raw-prism target asks, for each concrete oriented cyclic family T, for a 2-chain b with ∂b equal to the directed cycle of T minus an integer multiple of the fundamental cycle. The zero-winding bound is the geometric filling statement: every 1-cycle of winding zero is homologous to zero.
Upstream, raw prism generation transports categorically through toCycles to the cycle-object generation target; filling those oriented families then implies the zero-winding bound.
proof idea
One-line term composition. Apply orientedCyclicFamilies_boundary_generate_of_rawPrism to the raw-prism hypothesis to obtain the oriented-cyclic-family boundary-generation target (pure transport through toCycles). Feed that into zeroWindingCycles_bound_of_orientedCyclicFamilies, which itself reduces via the fundamental-cycle boundary generator to the zero-winding filling statement. No new geometric construction occurs here.
why it matters
Closes one link in the generation half of the integer comparison H₁(S¹;ℤ) ≅ ℤ: raw prism data on oriented cyclic families imply every zero-winding singular 1-cycle bounds. Downstream, zeroWindingCycles_bound_of_explicitRawPrism specializes this to a fully explicit raw-prism construction, so any concrete prism builder only needs to hit the raw target.
In the module narrative this is the filling theorem that subdivision/prism machinery must supply once the kills-boundaries identity and the winding left-inverse are in hand. It does not itself touch the Recognition forcing chain (T0–T8) or the J-cost; it is pure singular-homology infrastructure for the circle, on which later RS geometric arguments can rest when they need H₁(S¹) ≅ ℤ without axioms or project-local sphere replacements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.