zeroFlow_decomposesIntoCyclicEdgeLists
plain-language theorem explainer
The zero free singular 1-chain on S¹ equals the empty sum of cyclic edge-list terms. Anyone running the support-decreasing induction that decomposes finite edge-flows into certified cycles cites this as the base case. The proof is the one-line witness of the empty list with definitional equality.
Claim. There exists a finite list $ts$ of cyclic singular edge-list terms such that the zero element of the free $\mathbb{Z}$-module on singular $1$-simplices of $S^1$ equals the free-chain sum associated to $ts$. Explicitly, the empty list works.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Free edge-flows live in singularOneChainFree, the free $\mathbb{Z}$-module on actual singular $1$-simplices of TopCat.sphere 1.
A cyclic singular edge-list term packages a finite list of singular $1$-simplices, an integer coefficient, and a certified cycle whose free-chain image is that coefficient times the listed edge sum, together with an integrality witness for the cycle winding. The associated list-sum map sends the empty list to $0$ and otherwise accumulates coefficient-scaled edge-list chains.
The surrounding development aims at decomposing arbitrary finite-support free edge-flows into such certified cyclic pieces by induction on support cardinality. The zero flow is the natural base of that induction.
proof idea
One-line term proof. Witness the empty list of cyclic edge-list terms; definitional unfolding of the list-sum map on [] yields $0$, so reflexivity closes the equality.
why it matters
This is the base case for the support-decreasing finite-flow induction that decomposes free edge-flows into cyclic edge-list terms. The immediate parent is supportCard_zero_decomposesIntoCyclicEdgeLists, which reduces a support-cardinality-zero flow to the zero chain and applies this lemma.
In the broader CircleWindingChain program, such decompositions feed the winding homomorphism on $1$-cycles and the split-injective comparison with the fundamental class (the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ already obtained from covering-space winding). Surjectivity of the integer comparison map remains open and needs a simplicial prism or subdivision operator not yet in Mathlib singular homology. The lemma itself is pure chain bookkeeping, not a new topological identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.