orientedCyclicFamilyExtraction
plain-language theorem explainer
Any nonzero free singular 1-cycle on S¹ peels off one concrete oriented closed walk, leaving a residual cycle of strictly smaller ℓ¹ size. Homology and flow-decomposition arguments cite this as the inductive step that turns balanced edge-chains into finite lists of oriented cyclic families. The proof packages an existing existence lemma into a term, subtracts, and invokes the ℓ¹-decrease identity.
Claim. Let $c$ be a free singular $1$-chain on $S^1$ with vanishing free boundary and $c \neq 0$. Then there exist an oriented cyclic family $T$ (a finite sign-oriented closed walk of singular $1$-simplices) and a residual free $1$-chain $r$ such that $c = \mathrm{chain}(T) + r$, the free boundary of $r$ vanishes, and the $\ell^1$ size of $r$ is strictly smaller than that of $c$.
background
The 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}$. Free singular $1$-chains are finite $\mathbb{Z}$-linear combinations of singular $1$-simplices; the free boundary map is the usual alternating face operator on those generators.
An oriented cyclic family is a finite list of sign-oriented singular edges whose terminals match the next initials under cyclic rotation, i.e. a concrete closed oriented walk. Its associated free chain is the sum of those signed edges. The $\ell^1$ size chainL1 is the sum of absolute coefficients over the edge support.
Upstream, existence of such a walk inside any balanced nonzero flow is already available, as is the identity that subtracting the walk through $k$ distinct supported edges lowers $\ell^1$ by exactly $k$.
proof idea
Call the existence lemma for a balanced nonzero free cycle to obtain length $k$, an injective map $g$ into the edge support, and the cyclic incidence data. Orient each edge by the sign of its coefficient in $c$, package the resulting closed walk as an OrientedCyclicFamilyTerm $T$, and set the residual $r := c - \mathrm{chain}(T)$.
The sum identity is pure abelian arithmetic. Boundary of $r$ vanishes because both $c$ and $\mathrm{chain}(T)$ are cycles (the latter by the free-boundary vanishing lemma for oriented cyclic families). Strict $\ell^1$ decrease is chainL1_sub_orientedCyclic rewritten along the definition of $T$'s chain, finished by omega.
why it matters
This is the one-step inductive engine for freeBoundaryKernel_decomposesIntoOrientedCyclicFamilies_holds: every balanced free edge-chain decomposes into a finite list of concrete oriented cyclic families. That decomposition is the finite-flow theorem needed before translating signed oriented cycles into the older one-scalar cyclic-edge-list interface used in the generation half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
In the module's program, winding already kills boundaries and hits the fundamental loop; the remaining obstruction is expressing every $1$-cycle as an integer multiple of the fundamental class up to homology. Oriented extraction supplies the combinatorial peeling that makes the free kernel finitely generatable by closed walks, without Mathlib's missing simplicial prism operator. It sits entirely inside the Foundation circle-winding chain and does not itself touch the forcing chain T0–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.