orientedCyclicFamilies_freePrism_generate_of_splitCorrections
plain-language theorem explainer
The terminal-side and path-base correction targets together imply the free-coordinate prism generation target for every oriented cyclic family. Anyone assembling the Phase 5 generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ cites this reduction. The proof is a pure composition: split corrections fill the path-cone residual, which then yields the free prism.
Claim. Assume every oriented cyclic family $T$ admits a free $2$-chain whose boundary realizes the terminal-side correction residual (up to a fundamental-cycle multiple), and a free $2$-chain whose boundary replaces the path-parametric base edges by the signed oriented edge chain. Then every such $T$ admits a free $2$-chain $B$ with free boundary equal to the oriented edge sum minus the free-coordinate image of the matching fundamental cycle.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half needs an explicit simplicial prism: for each oriented cyclic family $T$, a free $2$-chain whose free boundary is the oriented edge sum minus the free image of the matching fundamental cycle (the free-prism target).
That residual is attacked by splitting. The terminal-side correction asks for a $2$-chain turning terminal-return sides into terminal constant sides (up to a fundamental-cycle multiple). The path-base correction asks for a $2$-chain replacing path-parametric base edges by the signed oriented singular-edge chain. Upstream, those two fill the full path-cone residual; filling the path-cone residual then proves the free-prism target.
proof idea
One-line term composition. First apply the split-to-path-cone lemma: the two hypotheses yield orientedCyclicFamilies_pathConeCorrection_generate. Feed that into the path-cone-to-free-prism lemma, which for each family $T$ takes a path-cone filler $K$ and returns the free prism chain $T.\mathrm{pathConeChain}-K$. No new chain algebra is done here.
why it matters
Closes the last logical gap between the two concrete correction halves and the Phase 5 free-prism checklist item. Downstream, orientedCyclicFamilies_freePrism_generate_holds instantiates both correction halves as proved and quotes this theorem to obtain the free-prism target unconditionally: every oriented cyclic family bounds the desired free-prism residual. That is the hand-built finite prism step Mathlib singular homology does not supply, and it is the generation half needed (with the already-proved kills-boundaries identity and the fundamental-loop winding) for the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.