directedCycleExtraction
plain-language theorem explainer
Every nonzero balanced free edge-flow on S¹ splits as one directed-cycle piece plus a balanced residual of strictly smaller ℓ¹ norm. Homology workers cite it as the peel step in the free-boundary kernel decomposition that feeds the integer comparison for H₁(S¹;ℤ). The argument packages an oriented closed walk from the balanced-flow cyclic-family lemma and applies the exact ℓ¹-drop identity for that walk.
Claim. Let $c$ be a free singular $1$-chain on $S^1$ with vanishing free boundary and $c \neq 0$. Then there exist a directed-cycle free term $t$ and a residual free $1$-chain $r$ such that $c = t.\mathrm{chain} + r$, the free boundary of $r$ is zero, and $\ell^1(r) < \ell^1(c)$.
background
This module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The free-chain side works with actual singular $0$- and $1$-simplices of that simplicial set, free modules on those simplices, and the explicit free boundary map.
A directed-cycle free term packages a multi-edge oriented closed walk as a free $1$-chain that is the image of an integral cycle, with integral winding. The size measure $\mathrm{chainL1}$ is the sum of absolute coefficients over the edge support. Upstream, $\mathrm{chainL1_sub_orientedCyclic}$ states that subtracting an oriented closed walk through $k$ distinct supported edges lowers $\ell^1$ by exactly $k$. The cyclic-family boundary lemma says such an oriented closed family has free boundary zero.
proof idea
From nonzero balanced $c$, invoke the existence of an oriented cyclic family of $k$ distinct supported edges with consecutive terminals matching initials. Orient each edge by the sign of its coefficient in $c$, and package the family as a directed-cycle free term $t$ whose chain equals the oriented cyclic chain of that family. Boundary of $t.\mathrm{chain}$ vanishes by the cyclic oriented-family free-boundary lemma. Take residual $r:=c-t.\mathrm{chain}$: the sum identity is abelian cancellation; residual balance is linearity of the free boundary plus both summands balanced. Strict $\ell^1$ decrease is $\mathrm{chainL1_sub_orientedCyclic}$ plus $k\ge 1$, finished by omega.
why it matters
Parent theorem $\mathrm{freeBoundaryKernel_decomposesIntoDirectedCycles_holds}$ runs strong induction on $\ell^1$, peeling one oriented closed walk per step via this extraction, and concludes every free edge-chain in the free-boundary kernel is a finite sum of directed-cycle pieces. That decomposition discharges the hypothesis of $\mathrm{circleH1ZIsoInt_of_directedCycles_of_zeroWinding_bounds}$, closing the generation/surjectivity half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ without axioms. In the module narrative this is the missing converse to the winding left-inverse coming from $\mathrm{simplexDisplacement_boundary}$ and the fundamental-loop normalization. Framework-wise it is pure singular-homology infrastructure on $S^1$, not a T0–T8 forcing step, but it underwrites the circle's first homology as $\mathbb{Z}$, the topological home of the eight-tick/octave winding story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.