singletonSupportFlow_decomposesIntoCyclicEdgeLists
plain-language theorem explainer
Any free singular 1-chain on S¹ whose edge support is a singleton and whose boundary vanishes equals a finite list of cyclic edge-list terms (in practice one term). Homology and circle-winding arguments cite it as the singleton base of the support-decreasing induction that generates H₁(S¹;ℤ). The proof reduces the chain to a scalar multiple of a free generator and invokes the single-edge flow decomposition.
Claim. Let $c$ be a free singular $1$-chain on $S^1$ and $e$ a singular $1$-simplex such that the edge support of $c$ is exactly $\{e\}$ and the free singular boundary of $c$ is zero. Then there exists a finite list $ts$ of cyclic singular edge-list terms with $c$ equal to the free-chain sum of that list.
background
The module lifts path-level winding on the circle to singular simplices of $S^1$ and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Free $1$-chains are finitely supported integer combinations of singular $1$-simplices; edgeSupport is that finite support and edgeCoeff reads the coefficient of a given edge.
A CyclicSingularEdgeListTerm packages a finite list of singular $1$-simplices, an integer coefficient, a certified $1$-cycle, and the identity that the free image of the cycle is the coefficient times the listed edge sum, plus an integrality witness for the cycle winding. The list-sum cyclicSingularEdgeListTermListChain folds those pieces into a free chain.
The local goal is to decompose every balanced free edge-flow into such cyclic pieces by induction on support size. The singleton-support case is the nontrivial base of that induction, stated in the native support language rather than as a bare free generator.
proof idea
From singleton support, $e$ lies in the support, so its coefficient $n:=\mathrm{edgeCoeff}(c,e)$ is nonzero. Extensionality of finitely supported functions shows $c$ equals the single Finsupp term at $e$ with value $n$. That term is rewritten as the module scalar $n\cdot\mathrm{freeMk}(e)$. Substituting into the boundary-vanishing hypothesis and the goal reduces exactly to singleEdgeFlow_decomposesIntoCyclicEdgeLists applied to $e$, $n$, the nonzero coefficient, and the rewritten boundary hypothesis.
why it matters
This is the singleton arm of the support-cardinality base case. Downstream, supportCard_le_one_decomposesIntoCyclicEdgeLists cases on support size $0$ or $1$ and invokes this theorem for the size-$1$ branch, packaging both base cases for the support-decreasing induction that decomposes balanced free edge-flows into cyclic edge-list pieces.
In the module's program that is the generation half of $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 supplies the left inverse to the fundamental class; cyclic edge-list decomposition is the combinatorial engine toward surjectivity of the integer comparison map. The module notes that full generation still needs a simplicial prism or subdivision operator that Mathlib's singular homology does not yet provide, so this lemma closes a proved base step rather than the whole generation theorem.
Framework-wise it sits in the Foundation circle-winding chain that underwrites the eight-tick octave and the topological side of the forcing chain, not in the J-cost or mass-ladder arithmetic directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.