orientedCyclicFamilies_terminalSideCorrection_generate
plain-language theorem explainer
Packages the terminal-side correction generation target: every oriented cyclic family admits a free singular 2-chain whose boundary turns the sum of terminal-return sides into the terminal constant sides, up to an integer multiple of the fundamental cycle. Downstream split-correction lemmas cite it when assembling free-prism generation for the surjectivity half of H₁(S¹;ℤ) ≅ ℤ. It is a bare Prop definition, not a proved statement.
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 of $K$ equals the terminal-side correction boundary of $T$ evaluated at $n$.
background
The ambient 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 fact that the once-around loop has winding $1$, this yields a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$. The remaining generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs explicit $2$-chains from prism and cone constructions.
Here the free singular $2$-chain group is the free $\mathbb{Z}$-module on singular $2$-simplices of $\mathrm{TopCat.sphere},1$, and the free boundary map sends each generator to the alternating sum of its three singular $1$-faces. An oriented cyclic family term records a closed chain of singular edges with lift data; its terminal-side correction boundary is the $1$-chain that replaces the sum of terminal-return sides by the terminal constant sides, corrected by a multiple of the fundamental cycle.
proof idea
Definitional packaging only: the body is the universal-existential Prop above. No tactics or lemmas are invoked. The concrete existence proof lives in the sibling theorem that discharges this target by assembling lift-affine cones, winding-step prisms, and connectivity integers from the family's cyclic lift data.
why it matters
This target is one of the two split correction hypotheses feeding the path-cone residual and then the Phase 5 free-prism generation target. The free-prism theorem states that the two split corrections (terminal-side and path-base) suffice for free-prism generation; the path-cone theorem states they jointly fill the full path-cone residual. Closing those targets is the constructive route to the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ that Mathlib's singular homology API does not yet supply via subdivision. The companion _holds theorem asserts the target is true unconditionally for every oriented cyclic family, so this Prop is the named interface those lemmas quantify over rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.