orientedCyclicFamilies_pathConeCorrection_generate_of_splitCorrections

This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices and proves that displacement kills boundaries of singular $2$-simplices. That fact supplies the homology-invariant half of the comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; the generation half needs a simplicial prism / subdivision operator that Mathlib singular homology does not yet provide, so the module builds free-coordinate prism targets by hand.

An oriented cyclic family packages the singular edge data of a cyclic walk on the circle. Three Prop-valued correction targets appear: the path-cone residual (a $2$-chain whose boundary matches the residual between summed path-cone boundary and the desired free-prism boundary), the terminal-side correction (turning terminal-return sides into constant terminal sides up to a fundamental-cycle multiple), and the path-base correction (replacing path-parametric base edges by the signed oriented singular-edge chain).

The residual identity used here equates the path-cone residual boundary with the terminal-side correction boundary after the path-base discrepancy is accounted for, so the two split targets are algebraically enough for the full residual.

Fix an oriented cyclic family $T$. From the terminal-side hypothesis extract an integer coefficient $n$ and a $2$-chain $K_s$ with the stated terminal-side boundary. From the path-base hypothesis extract a $2$-chain $K_p$ whose boundary is the path-base discrepancy. The candidate witness is the sum $K_s+K_p$ at the same $n$. Boundary is a module homomorphism, so it splits over the sum; substitute the two boundary equations and rewrite the path-cone residual via the residual-equals-terminal-side identity. Unfold the terminal-side correction boundary definition and finish by abelian normal form on the free chain group.

This is the glue step that turns the two split correction obligations into the single path-cone residual target. Downstream, orientedCyclicFamilies_freePrism_generate_of_splitCorrections applies it and then the path-cone-to-free-prism implication, with doc-comment: "The two split correction targets are enough for the Phase 5 free-prism generation target."

In the broader Recognition foundation this is part of the generation half of the winding comparison on $H_1(S^1;\mathbb{Z})$: once free-prism generation is available, every $1$-cycle is homologous to an integer multiple of the fundamental cycle, completing the split-injective winding map already obtained from kills-boundaries plus the once-around generator. The eight-tick / $D=3$ forcing chain is not invoked here; the local stake is purely the singular-homology generation infrastructure that later recognition and alpha-band arguments rely on for circle topology.