supportCard_le_one_extractionStep
plain-language theorem explainer
A nonzero free singular 1-chain that is a cycle and has edge-support size at most one is already a single closed edge with integer coefficient: it factors as one cyclic edge-list term plus a strictly smaller residual cycle (here the zero chain). Anyone proving support-decreasing extraction of balanced edge-flows into cyclic lists cites this base case. The proof collapses the support to a singleton, reads off the loop condition from vanishing boundary, and packages the edge via the loop constructor.
Claim. Let $c$ be a free singular $1$-chain on $S^1$ with vanishing singular boundary, $c \neq 0$, and with at most one edge in its support. Then there exist a cyclic singular edge-list term $t$ and a residual free $1$-chain $r$ such that $c = t.{\rm chain} + r$, the boundary of $r$ vanishes, and the edge-support cardinality of $r$ is strictly smaller than that of $c$.
background
The module lifts path winding on $S^1$ to singular $1$-simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. Parallel to that homology story, free edge-flows (explicit free $C_1$ chains) are decomposed into cyclic edge lists so winding can be read termwise.
Edge support is the finite set of singular $1$-simplices with nonzero coefficient; edgeCoeff is the integer coefficient of a given edge. A cyclic singular edge-list term packages a finite list of edges, a global integer coefficient, and a certified cycle whose free-chain image is that coefficient times the listed edge sum, together with an integral winding witness.
When a supported edge has equal initial and terminal faces, it is already a loop. The constructor cyclicSingularEdgeListTerm_of_loop turns such a closed edge and coefficient into a cyclic term without successor search. The present lemma is the support-cardinality $\le 1$ branch of one-step extraction for balanced free flows.
proof idea
From $c \neq 0$ and the card-zero characterization, support cardinality is nonzero; with the hypothesis $\le 1$ one gets equality to $1$. Finset card-one yields a unique supported edge $e$ with nonzero coefficient. Extensionality of Finsupp shows $c$ equals the single-edge chain on $e$.
That single is a scalar multiple of the free generator on $e$. Boundary zero on $c$ transfers to the scaled generator, so the single-edge flow lemma forces terminal face equal initial face: $e$ is a loop. Build $t$ by cyclicSingularEdgeListTerm_of_loop with coefficient edgeCoeff c e. Take residual $r = 0$. The three goals are: $c$ matches $t$'s chain (by the single-edge rewriting), boundary of zero vanishes, and support card of zero is $0 < 1$.
why it matters
This closes the small-support base case of cyclic edge-list extraction for free balanced $1$-flows on the circle. Downstream, cyclicEdgeListExtractionStep_of_largeSupport reduces the full extraction step to the large-support case by case-splitting on support size and invoking this theorem when the card is at most one (the doc notes the $\le 1$ cases are already closed and packages the handoff so later work only treats repeated-vertex extraction for large support).
In the module's program, extraction feeds the generation half of the integer comparison $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$: every $1$-cycle should be homologous to an integer multiple of the fundamental cycle. Winding already kills boundaries and hits the generator; support-decreasing decomposition into cyclic lists is the combinatorial engine for the converse. The lemma is pure singular-chain bookkeeping on $S^1$, not a physics constant claim, but it sits in the foundation layer that underwrites the circle's homology used throughout the Recognition chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.