chainL1_orientedCyclicChain
plain-language theorem explainer
The ℓ¹ norm of an oriented cyclic chain built from an injective family of k singular 1-simplices equals k. Anyone tracking cycle-peeling or flow decomposition on free singular 1-chains cites this size identity. The proof rewrites the support as the image of the family, shows each coefficient has absolute value 1, and counts the image by injectivity.
Claim. Let $c$ be a free singular $1$-chain on $S^1$ and let $g:\mathrm{Fin}\,k\to\{\text{singular $1$-simplices}\}$ be injective. Then the $\ell^1$ size of the oriented cyclic chain determined by $c$ and $g$ equals $k$.
background
This module lifts path-level winding on the circle to singular simplices of $S^1$ and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Alongside that homology story, the file develops an explicit free $C_1$ calculus used for cycle peeling of balanced flows.
The $\ell^1$ size chainL1 of a free edge-chain is the sum of absolute values of its integer coefficients over the edge support. The oriented cyclic chain associated to a flow $c$ and an injective family $g$ of $k$ edges places, on each edge in the image of $g$, the sign-unit of $c$'s coefficient (and zero off the walk). Upstream, edgeCoeff_orientedCyclicChain records that pointwise rule, and edgeSupport_orientedCyclicChain identifies the support with the image of $g$.
proof idea
Unfold chainL1 to a sum of absolute coefficients over the edge support. Replace the support by the image of $g$ via edgeSupport_orientedCyclicChain. For every edge in that image, edgeCoeff_orientedCyclicChain plus the sign-unit absolute-value lemma gives coefficient absolute value $1$. The sum therefore collapses to the cardinality of the image; injectivity of $g$ and Fintype.card_fin yield exactly $k$.
why it matters
This is the size identity behind one directed-cycle peel. Downstream, chainL1_sub_orientedCyclic uses it to prove that subtracting the oriented closed walk from a balanced flow lowers $\ell^1$ size by exactly $k$: each walk edge loses one unit of magnitude because signs align, and off-walk coefficients are untouched.
In the module's larger program, controlled $\ell^1$ decrease is the combinatorial engine that decomposes balanced free $1$-chains into oriented cycles, feeding the generation/surjectivity half of the integer comparison map for $H_1(S^1;\mathbb{Z})$. The module already has the kills-boundaries identity and the fundamental-loop normalization; cycle peeling is the remaining constructive route toward every $1$-cycle being homologous to an integer multiple of the fundamental class, without waiting on Mathlib's missing simplicial prism operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.