chainL1_sub_orientedCyclic
plain-language theorem explainer
Peeling one oriented closed walk of k distinct supported edges from a free singular 1-chain reduces the ℓ¹ mass by exactly k. Cycle-extraction arguments for balanced edge-flows on S¹ cite this identity as the strict descent step. The proof is pointwise magnitude additivity on the support, then Finset sum comparison against the residual and the walk.
Claim. Let $c$ be a free singular $1$-chain on $S^1$, and let $g:\{0,\ldots,k-1\}\to$ (singular $1$-simplices) be injective with each $g(i)$ in the edge support of $c$. If $P$ is the oriented cyclic chain built from $c$ and $g$ (unit coefficients aligned with the signs of $c$), then $\|c-P\|_1+k=\|c\|_1$.
background
The module lifts path winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Free edge-chains are finitely supported integer combinations of singular $1$-simplices; the edge support is the finite set of simplices with nonzero coefficient.
The $\ell^1$ size chainL1 is the sum of absolute coefficients over that support. An oriented cyclic chain through an injective family $g$ of $k$ supported edges places a unit coefficient of matching sign on each $g(i)$ and zero elsewhere; upstream, its $\ell^1$ size is exactly $k$. The present identity quantifies how much mass drops when that walk is subtracted from $c$.
proof idea
Write $P$ for the oriented cyclic chain. On every edge $e$ in the support of $c$, compare coefficients of $c$, $c-P$, and $P$. Using the coefficient formula for oriented cyclic chains: if $e$ lies on the image of $g$, the $P$-coefficient is the sign unit of $c$'s coefficient, so $|c_e|=|c_e-\mathrm{sign}(c_e)|+1$; off the image, $P$ vanishes and absolute values match. Supports of both $c-P$ and $P$ sit inside the support of $c$, so the two $\ell^1$ sums extend from their own supports to that common Finset. Summing the pointwise identity and invoking the upstream fact that $|P|_1=k$ yields $|c-P|_1+k=|c|_1$.
why it matters
This is the quantitative descent step for directed-cycle peeling on free balanced $1$-chains. Downstream, directedCycleExtraction packages one oriented closed walk plus a balanced residual of strictly smaller $\ell^1$ size, citing this identity for the drop; orientedCyclicFamilyExtraction keeps the family data in the same one-step split. Together they underwrite inductive extraction of cycle summands from nonzero balanced flows, which is the combinatorial engine behind identifying integer winding on $1$-cycles.
In the module's larger program, winding on singular $1$-simplices is already a homology invariant (kills boundaries) and sends the fundamental loop to $1$. Cycle extraction supplies the generation direction needed for the comparison map $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$ to be surjective once prism/subdivision technology is available. No T0–T8 forcing step is invoked here; the result is pure singular-chain bookkeeping on the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.