supportCard_le_one_decomposesIntoCyclicEdgeLists
plain-language theorem explainer
Any balanced free singular 1-chain whose edge support has size at most one equals a finite sum of concrete cyclic edge-list pieces. Homology workers extracting integer winding on S¹ cite this as the base of the support-decreasing induction that builds the cycle decomposition. The proof is a two-way case split on support cardinality 0 versus 1, dispatching each arm to an existing base lemma.
Claim. Let $c$ be a free singular $1$-chain on $S^1$. If the cardinality of its edge support is at most $1$ and the free singular boundary of $c$ vanishes, then there exists a finite list of cyclic edge-list terms whose free-chain sum equals $c$.
background
The 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}$. Free singular $1$-chains are finitely supported integer combinations of singular $1$-simplices; edgeSupport is that finite support, and edgeSupportCard is its cardinality.
A balanced chain means the free singular boundary vanishes. A CyclicSingularEdgeListTerm packages a finite list of singular edges, an integer coefficient, and a certified cycle whose free image is that coefficient times the listed edge sum, together with an integral winding witness.
The list-sum cyclicSingularEdgeListTermListChain folds those pieces into one free chain. The extraction target cyclicEdgeListExtractionStep asks that every nonzero balanced free edge-flow split as one such cyclic piece plus a balanced residual of strictly smaller support; the present theorem supplies the support-size $\le 1$ base of that induction.
proof idea
From edgeSupportCard c ≤ 1, omega yields the dichotomy card $=0$ or card $=1$.
If the support is empty, apply the zero-support decomposition lemma, which returns the empty list of cyclic terms.
If the support has cardinality one, Finset.card_eq_one produces the unique edge $e$ in the support; feed $c$, $e$, the singleton-support equality, and the boundary-vanishing hypothesis into singletonSupportFlow_decomposesIntoCyclicEdgeLists, which builds the cyclic list for a single supported edge flow.
why it matters
This packages the zero and singleton base cases for the support-decreasing induction that proves every balanced free edge-flow decomposes into cyclic edge-list pieces. Downstream, largeSupportCyclicEdgeListExtractionStep_of_uniformOriented uses the extraction machinery whose base rests here; that theorem isolates the remaining finite-flow obstruction to uniform orientation of the extracted cycle.
In the module's larger program, such a decomposition lets the winding homomorphism on $1$-cycles act termwise and recover the integer comparison map that is a left inverse to the fundamental class. That is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ already advertised in the module doc. The generation (surjectivity) half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply; the present base case does not close that gap, but it clears the small-support obstruction on the extraction path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.