singleEdgeFlow_decomposesIntoCyclicEdgeLists
plain-language theorem explainer
A nonzero integer multiple of one singular 1-simplex on S¹ with vanishing free boundary is already a one-term cyclic edge-list. The singleton-support flow extractor cites this as the cardinality-one base of finite-flow decomposition. Proof equates the two faces, packages the edge as a loop term, and checks the list-chain identity by simplification.
Claim. Let $e$ be a singular $1$-simplex on $S^1$ and $n\in\mathbb{Z}\setminus\{0\}$. If the free chain $n\cdot e$ has vanishing singular boundary, then there is a finite list of cyclic singular edge-list terms whose free-chain sum equals $n\cdot e$.
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}$. A singular one-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$.
A cyclic singular edge-list term packages a finite list of such edges, an integer coefficient, a certified $1$-cycle, and the identity that the free image of that cycle is the coefficient times the listed edge sum, plus an integrality witness for the cycle winding. The free-chain sum of a list of such terms is defined recursively: empty list is zero; head plus tail adds the scaled edge-list chain of the head.
Upstream, a single edge whose two face maps agree is already such a term via the loop constructor: no successor search is needed when the supported edge is closed. Zero free boundary on a scaled single edge forces those faces equal.
proof idea
From vanishing boundary of $n\cdot e$ with $n\neq 0$, apply the face-equality lemma for single-edge flows to obtain terminal face equals initial face. Feed that equality into the loop-term constructor to build one cyclic edge-list term with coefficient $n$ and edge list $[e]$. Exhibit the singleton list of that term. Unfold the list-chain and loop-term definitions; simplification reduces both sides to $n$ times the free generator on $e$.
why it matters
This is the support-cardinality-one subcase of finite-flow extraction on free $1$-chains of $S^1$. The immediate parent is the singleton-support flow theorem, which restates the same conclusion in edgeSupport language for the support-decreasing induction: any balanced free edge-flow with support ${e}$ is a one-term cyclic edge-list.
In the module arc, cyclic edge-list decompositions feed the generation half of the integer comparison map on $H_1(S^1;\mathbb{Z})$: every $1$-cycle should be homologous to an integer multiple of the fundamental cycle. The winding side (kills-boundaries plus generator to $1$) is already in place; flow extraction supplies the concrete cycle representatives the generation argument needs. No T0–T8 forcing step is touched directly; the result is pure singular-homology infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.