orientedCyclicFamilies_pathBaseCorrection_generate
plain-language theorem explainer
The path-base correction target asks that every oriented cyclic family term admit a free singular 2-chain whose boundary replaces path-parametric base edges by the signed oriented singular-edge chain. Circle-homology workers cite it when assembling free-prism and path-cone generation. It is a bare Prop definition: a universal residual-filling statement, not a proved theorem.
Claim. For every oriented cyclic family term $T$, there exists a free singular $2$-chain $K_p$ on $S^1$ such that $\partial_2 K_p = C_{\mathrm{path\text{-}base}}(T) - C_{\mathrm{oriented}}(T)$, where $\partial_2$ is the alternating face-sum boundary $C_2^{\mathrm{free}}(S^1;\mathbb{Z})\to C_1^{\mathrm{free}}(S^1;\mathbb{Z})$.
background
The module lifts path-level winding on $S^1$ to singular simplices. Displacement of a singular $1$-simplex is path displacement after reparameterising $\Delta^1$ to $[0,1]$; the key identity is that alternating face sums of every singular $2$-simplex have vanishing displacement (winding kills boundaries). Together with the fundamental loop sending to $1$, this gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Generation (surjectivity of the integer comparison) needs prism and subdivision corrections. Free singular $2$-chains are the free $\mathbb{Z}$-module on actual singular $2$-simplices of $\mathrm{TopCat.sphere},1$; the free boundary sends each generator to $\delta_0-\delta_1+\delta_2$. An oriented cyclic family term packages a finite family of oriented singular edges with both a path-parametric base edge chain and a signed oriented edge chain; their difference is the residual this target asks to fill.
proof idea
No proof: the declaration is a Prop definition. Its body is the universal statement that every oriented cyclic family term $T$ has some free $2$-chain $K_p$ with free boundary equal to the path-base edge chain of $T$ minus its oriented edge chain. Downstream, a sum identity shows the family residual equals the sum of edge-local path-base residuals, so edge-local fillers imply the family target; a separate holds theorem discharges the Prop via triangular backtrack prisms on reversed edges and zero residual on forward edges.
why it matters
This Prop is one of two split correction targets (with terminal-side correction) that feed path-cone correction and then Phase 5 free-prism generation for oriented cyclic families. Downstream, edge-local fillers imply the family target, and the holds theorem closes it: every reversed oriented edge is filled by a triangular backtrack prism and every forward edge has zero residual. The free-prism theorem then takes both split targets as hypotheses and obtains free-prism generation. In the module arc this is part of the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, complementary to the already-proved kills-boundaries / split-injective half from simplex displacement. It does not itself touch T0–T8 or the RCL; it is pure singular-chain scaffolding for the circle comparison map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.