orientedCyclicFamilies_pathBaseCorrection_generate_holds
plain-language theorem explainer
Every oriented cyclic family admits a free singular 2-chain whose boundary replaces its path-parametric base edges by the signed oriented singular-edge chain. Homology workers building the free-prism residual for circle H₁ cite this closure. The proof is a one-line application of the edge-local generator lemma to the triangular backtrack-prism bounds on each oriented edge.
Claim. For every oriented cyclic family term $T$, there exists a free singular $2$-chain $K_p$ such that $\partial_2 K_p = T^{\mathrm{path\text{-}base}} - T^{\mathrm{oriented}}$, i.e. the path-parametric base-edge chain is homologous to the signed oriented singular-edge chain.
background
This module lifts path-level winding and displacement on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. Combined with the once-around generator mapping to $1$, that yields the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation (surjectivity) half needs simplicial prisms and subdivision, which Mathlib singular homology does not yet supply.
The path-base correction target is the Prop asking, for each oriented cyclic family term $T$, for a free $2$-chain whose boundary equals the difference of the path-base edge chain and the oriented edge chain. An upstream reduction shows that edge-local corrections suffice: if every oriented singular edge $o$ has a $2$-chain with boundary equal to its path-base correction residual, the family-level target follows by summing.
Locally, reversed edges are filled by triangular backtrack prisms and forward edges contribute zero residual, so the edge-local hypothesis is available as an explicit boundary identity.
proof idea
One-line term wrapper. Apply the reduction orientedCyclicFamilies_pathBaseCorrection_generate_of_localEdges, which lifts a universal edge-local filler to the family-level Prop, and feed it the already-proved edge bounds OrientedSingularEdge.pathBaseCorrectionBoundary_bounds. No further case split or chain arithmetic appears at this layer.
why it matters
This closes one of the two correction halves needed for free-prism generation. Downstream, orientedCyclicFamilies_freePrism_generate_holds combines it with the terminal-side correction to conclude that every concrete oriented cyclic family bounds the desired free-prism residual. That free-prism step feeds the Mathlib circle-linking backend (mathlibCircleLinkingBackend_of_largeSupport_of_zeroWinding_bounds), which is required by the strict T8 replacement in the forcing chain (spatial dimension $D=3$).
In the module narrative, generation of $H_1(S^1;\mathbb{Z})$ is the half Mathlib does not yet provide; path-base correction is the residual that replaces path-parametric base edges by oriented singular edges inside that generation argument. Closing it unconditionally removes a scaffold from the circle-homology bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.