orientedCyclicFamilies_pathConeCorrection_generate
plain-language theorem explainer
Names the residual correction target after summing path-cones over an oriented cyclic family: every such family admits a free singular 2-chain whose boundary equals the residual between the summed path-cone boundary and the desired free-prism boundary (up to a fundamental-cycle multiple). Anyone closing the generation half of H₁(S¹;ℤ) ≅ ℤ via prism/subdivision cites this interface. Pure Prop packaging; no constructive content.
Claim. For every oriented cyclic family term $T$, there exist an integer $n$ and a free singular $2$-chain $K$ on $S^1$ such that the free singular boundary $\partial K$ equals the path-cone residual boundary of $T$ evaluated at $n$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. Together with the once-around generator mapping to $1$, this gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The surjective (generation) half needs a prism/subdivision operator that Mathlib singular homology does not yet supply.
Free singular $2$-chains are the free $\mathbb{Z}$-module on singular $2$-simplices of the topological circle. Their boundary map is the alternating sum of the three face operators. An oriented cyclic family packages a finite collection of paths whose concatenated winding is an integer; path-cones over that family produce a $2$-chain whose boundary is almost the free-prism boundary, leaving a residual $1$-cycle that must still be filled.
The residual boundary of a family term at integer $n$ is exactly that leftover: summed path-cone boundary minus the free-prism target, adjusted by $n$ times the fundamental cycle.
proof idea
Definitional Prop only. The body is the universal-existential formula: quantify over every oriented cyclic family term, then assert existence of an integer coefficient and a free $2$-chain whose image under the free singular boundary equals that term's path-cone residual boundary. No tactics, no lemmas applied.
why it matters
This is the Phase-5 correction interface that unlocks the generation half of the circle homology computation. Downstream, filling it implies the free-prism generation target, which in turn yields both the Mathlib comparison isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ and the zero-winding filling theorem (every zero-winding $1$-cycle bounds). It is itself discharged by splitting into terminal-side and path-base correction targets. In the broader Recognition foundation this closes the singular-chain side of the winding invariant, the missing surjectivity half flagged in the module doc after the kills-boundaries identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.