orientedCyclicFamilies_explicitRawPrism_generate_iff_zeroWindingCycles_bound
plain-language theorem explainer
Under decidable equality on singular 0- and 1-simplices of S¹, the fully explicit raw-prism generation target is equivalent to the zero-winding filling bound. Anyone closing the generation half of H₁(S¹;ℤ) ≅ ℤ cites this bridge. The proof is a two-line constructor applying the two one-direction lemmas already in the module.
Claim. Assuming decidable equality on singular $0$- and $1$-simplices of $S^1$, the following are equivalent: (i) every oriented cyclic family $T$ admits a singular $2$-chain $b$ whose boundary equals the raw oriented edge sum of $T$ minus the matching multiple of the fundamental $1$-cycle; (ii) every zero-winding $1$-cycle is a boundary (the zero-winding filling bound).
background
The module lifts path-level winding on $S^1$ to singular simplices. simplexDisplacement sends each singular $1$-simplex $f:C(\Delta^1,S^1)$ to a real displacement ($2\pi$ times winding) 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$ plus homotopy invariance and additivity of path displacement.
Together with the fact that the once-around generator has winding $1$, this yields a left inverse to the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a prism or subdivision filler, which Mathlib singular homology does not yet supply.
The explicit raw-prism target asks, for each oriented cyclic family term $T$, for a $2$-chain whose boundary is the free image of the oriented edge sum of $T$ minus the fundamental-cycle multiple. The zero-winding bound is the geometric filling statement that zero-winding cycles bound.
proof idea
Pure constructor on the biconditional. Left-to-right: introduce the explicit-raw hypothesis and apply zeroWindingCycles_bound_of_explicitRawPrism. Right-to-left: apply the already-proved orientedCyclicFamilies_explicitRawPrism_generate_of_zeroWindingCycles_bound, which itself routes through the boundary-generate intermediate. No new algebra; just packaging the two directions.
why it matters
This is the packaging step that equates the fully explicit raw-prism checklist item with the actual geometric zero-winding filling theorem. Downstream, orientedCyclicFamilies_freePrism_generate_iff_zeroWindingCycles_bound and orientedCyclicFamilies_rawPrism_generate_iff_zeroWindingCycles_bound cite it to collapse free-coordinate and packaged raw prism targets onto the same filling statement.
In the module narrative, the remaining gap for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is precisely that geometric filling construction (prism or subdivision). Equating the checklist formulations to zero-winding filling means only one geometric object still needs to be built. Within Recognition Science this sits in the Foundation layer that underwrites circle homology used by later forcing and octave arguments; it does not itself invoke T5–T8 or the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.