freeBoundaryKernel_decomposes
plain-language theorem explainer
Every free singular 1-chain on S¹ whose free boundary vanishes is a finite sum of closed singular edge cycles. Algebraic topologists chasing the generation half of H₁(S¹;ℤ) ≅ ℤ cite this Prop as the remaining finite-graph cancellation statement in free-module coordinates. It is a pure interface definition packaging that claim; no proof is attached.
Claim. The proposition asserting: for every element $c$ of the free $\mathbb{Z}$-module on singular $1$-simplices of $S^1$, if the free boundary of $c$ is zero, then there exists a finite list of closed singular one-cycle terms whose summed raw chain maps to $c$ under the raw-to-free comparison homomorphism.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half (every 1-cycle homologous to an integer multiple of the fundamental cycle) still needs a spanning statement for actual cycle representatives.
The free edge module is the free $\mathbb{Z}$-module on singular 1-simplices of $\mathrm{TopCat.sphere},1$. Its free boundary sends each directed edge to terminal 0-face minus initial 0-face. The raw singular chain group $C_1(S^1;\mathbb{Z})$ maps into that free module by sending each coproduct summand to the corresponding free generator. Closed singular one-cycle terms are the explicit closed-generator building blocks; a finite list of them assembles, by successive addition, to a raw $C_1$ chain.
The Prop packages the remaining finite graph/cancellation theorem in those free-module coordinates: kernel of free boundary equals the span of closed singular edge cycles.
proof idea
No proof body: the declaration is a bare Prop definition. It quantifies over free 1-chains, assumes free boundary zero, and asserts existence of a finite list of closed singular one-cycle terms whose assembled raw chain maps to the given free chain under the raw-to-free comparison. Downstream theorems take this Prop as a named hypothesis and discharge the spanning claim for raw cycle representatives by transporting along that comparison map.
why it matters
This is the last finite-cancellation interface needed before the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ can be stated for raw singular cycles. The module already has the kills-boundaries identity and the winding left-inverse on the fundamental loop; what remains is that every free boundary-zero 1-chain is a finite sum of closed edge cycles.
The sole immediate consumer is closedSingularOneChainList_spansCycles_of_freeBoundaryKernel_decomposes, whose doc-comment records that the free-boundary kernel decomposition implies the raw-chain spanning statement for actual cycle representatives. That spanning fact is the missing generation half flagged in the module doc: Mathlib still lacks the simplicial prism/subdivision operator that would prove it outright.
In the broader Recognition chain this sits in Foundation circle-winding work that underwrites discrete octave and homology bookkeeping (T7 eight-tick structure), not yet the forcing of $J$ or $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.