chainL1
plain-language theorem explainer
The ℓ¹ norm of a free singular 1-chain on S¹ is the sum of absolute integer coefficients over its edge support. Homology and cycle-extraction arguments cite it as the discrete size measure for induction. The body is a one-line Finset sum of natAbs of edge coefficients.
Claim. For a free singular $1$-chain $c$ on $S^1$ (an element of the free $\mathbb{Z}$-module on singular $1$-simplices), define $\|c\|_1 := \sum_{e \in \mathrm{supp}(c)} |c_e| \in \mathbb{N}$, where $c_e$ is the integer coefficient of edge $e$.
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}$.
A free edge-chain is an element of the free $\mathbb{Z}$-module on actual singular $1$-simplices of $\mathrm{TopCat.sphere},1$. The coefficient of an edge is the value of that finitely supported function; the edge support is the finite set where the coefficient is nonzero.
The $\ell^1$ size packages those data into a single natural number: sum of absolute coefficients. It is the discrete height used later to peel directed cycles from balanced flows.
proof idea
Definitional one-liner: unfold as the Finset sum, over the edge support of $c$, of the natural absolute value of each integer edge coefficient. No lemmas are applied beyond the supporting accessors for coefficient and support.
why it matters
This size is the induction measure for the unconditional directed-cycle decomposition of the free boundary kernel. Downstream, the $\ell^1$ of an oriented closed walk on $k$ distinct edges equals $k$, and subtracting that walk from a balanced flow drops $\ell^1$ by exactly $k$.
Those facts feed one-step directed-cycle extraction and oriented-cyclic-family extraction: every nonzero balanced free edge-flow splits as a cycle piece plus a strictly smaller residual. Strong induction on $\ell^1$ then yields that every free edge-chain in the kernel is a finite sum of directed-cycle pieces, discharging the hypothesis needed for the integer comparison map on $H_1(S^1)$ without axioms or sorry.
In the broader circle-winding chain, this is bookkeeping infrastructure for the generation half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$, complementary to the winding-kills-boundaries identity already proved at the simplex level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.