orientedCyclicFamilies_freePrism_generate_of_pathConeCorrection
plain-language theorem explainer
If every oriented cyclic family admits a free 2-chain correcting the path-cone residual, then the Phase 5 free-prism generation target holds: each such family has a free 2-chain whose free boundary is the oriented edge sum minus the free image of a matching fundamental cycle. Anyone closing the generation half of H₁(S¹;ℤ) ≅ ℤ cites this reduction. The proof subtracts the residual witness from the summed path-cone chain and cancels by abelian arithmetic.
Claim. Assume that for every oriented cyclic family $T$ there exist an integer $n$ and a free singular $2$-chain $K$ with free boundary equal to the path-cone residual of $T$ at $n$. Then for every such $T$ there exist an integer $n$ and a free singular $2$-chain $B$ whose free boundary equals the oriented edge sum of $T$ minus the free-coordinate image of $n$ times the fundamental cycle.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries of $2$-simplices. Together with the fact that the once-around loop has winding $1$, this gives 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 an explicit free prism / generation construction that Mathlib singular homology does not yet supply.
An oriented cyclic family packages a finite oriented edge sum on the circle. The free-prism generation target asks for a free $C_2$ chain whose free boundary is that edge sum minus the free image of a matching fundamental cycle. Summing path-cones over the family produces a candidate $2$-chain whose boundary differs from the desired free-prism boundary by a residual; the path-cone correction target is exactly the existence of a free $2$-chain filling that residual.
proof idea
Term-mode reduction, not a geometric construction. Fix an oriented cyclic family $T$. From the path-cone correction hypothesis obtain $n$ and a free $2$-chain $K$ with free boundary equal to the path-cone residual of $T$ at $n$. Take the free prism witness to be the difference of the family's summed path-cone chain and $K$.
Apply linearity of the free boundary map, rewrite via the residual identity, unfold the residual and desired free-prism boundary definitions (including the free image of the fundamental cycle), and finish by abelian cancellation (abel). The same integer $n$ is reused.
why it matters
This is the bridge from residual correction to the clean Phase 5 free-prism checklist item. Downstream, circleH1ZIsoInt_of_pathConeCorrection feeds the free-prism form into the full Mathlib comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The same reduction closes zero-winding filling via zeroWindingCycles_bound_of_pathConeCorrection, and is the last step in orientedCyclicFamilies_freePrism_generate_of_splitCorrections once side and path-base corrections are assembled into a path-cone residual.
In the Recognition foundation stack this is pure singular-homology bookkeeping for the circle generator: the winding invariant already kills boundaries and hits $1$ on the fundamental loop; generation supplies the missing surjectivity. No forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the payoff is a certified integer homology generator for later circle-based constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.