fundamentalCycle_boundary_generates_of_orientedCyclicFamilies
plain-language theorem explainer
Assuming every concrete oriented cyclic family is homologous to an integer multiple of the fundamental cycle, every singular 1-cycle on S¹ is homologous to such a multiple. Anyone proving the generation half of H₁(S¹;ℤ) ≅ ℤ cites this reduction. The proof maps a cycle to a free edge-chain, decomposes the boundary kernel into oriented families, then reassembles via injectivity of the cycle and free-chain maps.
Claim. Assume every oriented cyclic family term $T$ admits $n \in \mathbb{Z}$ and a singular $2$-chain $b$ with $T$ homologous to $n$ times the fundamental cycle plus $\partial b$. Then for every singular $1$-cycle $z$ on $S^1$, there exist $n \in \mathbb{Z}$ and a singular $2$-chain $b$ such that $z = \partial b + n\,[S^1]$.
background
The module lifts path winding on $S^1$ to singular $1$-simplices via simplexDisplacement (displacement $= 2\pi \times$ winding) and proves the kills-boundaries identity: the alternating face sum of displacement on any singular $2$-simplex vanishes. With the fundamental loop sending to winding $1$, this gives the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
The remaining generation half is packaged as fundamentalCycle_boundary_generates: every degree-$1$ cycle in Mathlib's singular integer chain complex of TopCat.sphere 1 equals a $2$-boundary plus an integer multiple of the fundamental cycle. A coarser local target, orientedCyclicFamilies_boundary_generate, asks only that each concrete oriented closed walk (oriented cyclic family) be homologous to such a multiple.
Upstream, every balanced free edge-chain decomposes into a list of oriented cyclic family terms (freeBoundaryKernel_decomposesIntoOrientedCyclicFamilies_holds). The free-chain image of a cycle-object list matches the explicit free-chain list (directedCycleFreeTermList_chain_eq).
proof idea
Fix a degree-$1$ cycle $z$. Push it through the cycles inclusion and the free-chain isomorphism to a free $1$-chain $c$. Commutation of free boundary with the complex differential plus iCycles_d shows $\partial c = 0$.
Apply the kernel decomposition to obtain a list ts of oriented cyclic family terms with $c$ equal to their free-chain sum. Injectivity of the free-chain map (it is an iso) and of iCycles (a mono) lifts that equality back to $z$ equal to the cycle-object list built from ts.
Invoke the list-level generator under the oriented-family hypothesis to get $n$ and a $2$-chain $b$ for that list, then transport along the identification of $z$ with the list cycle.
why it matters
This is the bridge from local geometric fillings of oriented closed walks to the global chain-level generation statement needed for $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. Downstream, circleH1ZIsoInt_of_orientedCyclicFamilies feeds the result into the final Mathlib circle $H_1$ computation ("the concrete oriented-family filling target is enough"), and zeroWindingCycles_bound_of_orientedCyclicFamilies closes the zero-winding filling target the same way.
In the Recognition Science forcing chain this supports the strict T8 spatial-dimension target via the singular homology of the circle: the generation half that Mathlib does not yet supply by prism/subdivision. The module doc frames surjectivity of the integer comparison map as the remaining geometric work; this theorem reduces that work to filling oriented cyclic families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.