supportCard_zero_decomposesIntoCyclicEdgeLists
plain-language theorem explainer
A free singular 1-chain on S¹ with empty edge support is exactly the empty list of cyclic edge-list pieces. Anyone running the support-decreasing induction on balanced edge-flows cites this as the zero base case. The proof rewrites support-cardinality zero to the zero chain and applies the zero-flow decomposition.
Claim. If $c$ is a free singular $1$-chain on $S^1$ and the cardinality of its edge support is $0$, then there exists a finite list $ts$ of cyclic singular edge-list terms such that $c$ equals the free-chain sum of that list (necessarily the empty sum, hence $c=0$).
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Free edge-chains live in the free $\mathbb{Z}$-module on actual singular $1$-simplices of $\mathrm{TopCat.sphere},1$.
edgeSupportCard is the finite cardinality of the Finsupp support of such a chain; edgeSupportCard_eq_zero_iff says that cardinality is zero exactly when the chain is the zero element. A CyclicSingularEdgeListTerm 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, with integral winding. The list-sum cyclicSingularEdgeListTermListChain folds those pieces (empty list maps to $0$).
proof idea
Three-line reduction. From edgeSupportCard c = 0, apply edgeSupportCard_eq_zero_iff to obtain $c=0$. Rewrite the goal under that equality, then discharge by zeroFlow_decomposesIntoCyclicEdgeLists, which supplies the empty-list witness for the zero free chain.
why it matters
This is the zero-support base case for decomposing balanced free edge-flows into cyclic edge-list pieces. Downstream, supportCard_le_one_decomposesIntoCyclicEdgeLists packages zero and singleton support as the base of a support-decreasing induction on balanced flows (boundary zero). That induction is part of the chain-level infrastructure that turns the winding/displacement invariant into a homology invariant on $1$-cycles, feeding the "kills boundaries" identity and the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the CircleWindingChain development. It does not itself touch the generation/surjectivity half, which still needs simplicial prism or subdivision operators absent from Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.