freeBoundaryKernel_decomposesIntoDirectedCycles_holds
plain-language theorem explainer
Every free singular 1-chain on S¹ that lies in the kernel of the explicit boundary map is a finite integer sum of directed closed walks. Algebraic topologists proving the generation half of H₁(S¹;ℤ) ≅ ℤ cite this to remove the finite-flow hypothesis from the winding comparison. The argument is strong induction on ℓ¹ mass, peeling one oriented cycle at each step via directed-cycle extraction.
Claim. Assuming decidable equality on singular $0$- and $1$-simplices of $S^1$, every free singular $1$-chain $c$ with $\partial c = 0$ admits a finite list of directed-cycle terms whose sum equals $c$. Equivalently, the kernel of the free boundary map on singular $1$-chains decomposes as a finite sum of oriented closed walks.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. Combined with the fact that the fundamental loop has winding $1$, this yields a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. The remaining generation half needs every $1$-cycle to be homologous to an integer multiple of the fundamental cycle.
Work is done in the free $\mathbb{Z}$-module on actual singular $1$-simplices of TopCat.sphere 1. The $\ell^1$ size chainL1 is the sum of absolute coefficients on the edge support. A directed-cycle free term packages one oriented closed walk as a free chain; the list-sum of such terms is the candidate decomposition of any boundary-closed free chain.
The extraction lemma supplies, for any nonzero free $1$-cycle, a single directed-cycle term $t$ and a strictly smaller-$\ell^1$ remainder $r$ still in the kernel, with $c = t.chain + r$. That size drop fuels the induction.
proof idea
Reduce to a strong induction on $n = \mathrm{chainL1}(c)$: every free $1$-chain of $\ell^1$ size $n$ with vanishing free boundary is a list-sum of directed-cycle terms. Apply the inductive statement at $n = \mathrm{chainL1}(c)$.
In the inductive step, if $c = 0$ return the empty list. Otherwise invoke directedCycleExtraction to obtain a directed-cycle term $t$ and remainder $r$ with $c = t.chain + r$, $\partial r = 0$, and $\mathrm{chainL1}(r) < n$. The inductive hypothesis on $r$ yields a list ts; cons $t$ onto ts and rewrite.
why it matters
This is the unconditional finite-flow theorem for free singular $1$-cycles on $S^1$. It discharges the directed-cycle decomposition hypothesis used by the integer winding comparison, so cycleWinding_integral_unconditional follows in one classical line: every singular $1$-cycle has integer winding with no extra finite-flow assumption.
Downstream, fundamentalCycle_boundary_generates_of_directedCycleTerms localizes the remaining geometric work: fill one directed closed walk, then sum witnesses. Together with the equivalence zeroWindingCycles_bound_iff_fundamentalCycle_boundary_generates, the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ reduces to a single closed-walk filling problem.
In the Recognition Science foundation stack this supplies the chain-level split of the circle's first homology that underwrites the winding invariant used throughout the circle-winding and eight-tick analyses. No axioms or sorry remain in the decomposition itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.