orientedCyclicFamilies_pathBaseCorrection_generate_of_localEdges
plain-language theorem explainer
If every oriented singular edge admits a free 2-chain whose boundary is its path-base correction, then every oriented cyclic family term has a free 2-chain correcting path-base edges to the signed oriented edge chain. Circle-homology workers closing the generation half of H₁(S¹;ℤ)≅ℤ cite this reduction. The proof sums the local fillings and invokes boundary linearity plus the family's path-base sum identity.
Claim. Assume that for every oriented singular edge $o$ there is a free singular $2$-chain $K$ with $\partial K$ equal to the path-base correction boundary of $o$. Then for every oriented cyclic family term $T$ there exists a free singular $2$-chain $K_T$ such that $\partial K_T$ equals the path-base edge chain of $T$ minus its oriented edge chain.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity, with the once-around generator mapping to $1$, gives the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Generation (surjectivity) needs prism/subdivision fillings that Mathlib singular homology does not yet supply.
An oriented singular edge pairs a singular $1$-simplex with a forward/backward traversal. The path-base correction target asks, for each oriented cyclic family term $T$, for a free $2$-chain whose boundary replaces $T$'s path-parametric base edges by the signed oriented singular-edge chain: $\partial K_T=T_{\mathrm{path\text{-}base}}-T_{\mathrm{oriented}}$. The local hypothesis is the same statement one edge at a time.
proof idea
Term-mode proof by summing local data. Fix a family term $T$. From the edge-local hypothesis, choose for each oriented edge $T.o,i$ a free $2$-chain $K_i$ with $\partial K_i$ equal to that edge's path-base correction boundary. Take $K_T=\sum_i K_i$. Boundary is linear, so $\partial K_T=\sum_i\partial K_i$. Congruence of the sum replaces each summand by the local correction boundary; the family's path-base correction boundary sum identity then identifies the total with $T_{\mathrm{path\text{-}base}}-T_{\mathrm{oriented}}$.
why it matters
This is the locality-to-family glue step for path-base corrections in the circle winding chain. The sole downstream consumer is orientedCyclicFamilies_pathBaseCorrection_generate_holds, which discharges the local hypothesis by triangular backtrack prisms on reversed edges and zero residual on forward edges, thereby closing the path-base correction target.
In the module's program that is one brick toward the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: injectivity is already proved via the covering-space winding invariant; surjectivity still needs simplicial prism/subdivision operators. The declaration itself is pure free-chain bookkeeping and does not touch the Recognition forcing chain (T5–T8) or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.