freeBoundaryKernel_decomposesIntoCyclicEdgeLists
plain-language theorem explainer
Every balanced free singular 1-chain on S¹ equals a finite integer combination of cyclic edge-list pieces. Homology workers closing the integer comparison H₁(S¹;ℤ) ≅ ℤ cite this as the remaining concrete finite-graph target. It is a named Prop (not a proved theorem); discharge is by support-decreasing cyclic extraction or the large-support extraction route.
Claim. For every free singular $1$-chain $c$ on $S^1$, if the free boundary of $c$ vanishes, then there exists a finite list of cyclic singular edge-list terms whose free-chain sum equals $c$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The free singular $1$-chain module is the free $\mathbb{Z}$-module on actual singular $1$-simplices of $\mathrm{TopCat.sphere},1$. Its free boundary sends each directed edge to the terminal $0$-face minus the initial $0$-face.
A cyclic singular edge-list term packages a coefficient with a closed edge walk. The list-chain map sums those pieces: empty list to zero, and head term plus recursive tail otherwise. "Balanced" here means free boundary zero, i.e. a free $1$-cycle in that module.
This Prop is the more concrete remaining finite-graph target: every such balanced free edge-flow decomposes into finitely many cyclic edge-list pieces, rather than an abstract directed-cycle sum.
proof idea
Named proposition, not a proved theorem. The body is a single universal quantifier: for every free singular $1$-chain with vanishing free boundary, assert existence of a finite list of cyclic edge-list terms whose free-chain sum recovers the chain.
No tactics run here. Downstream, the Prop is discharged by strong induction on support cardinality from a one-step cyclic extraction hypothesis, or reduced further to a large-support repeated-vertex extraction theorem.
why it matters
This is the concrete finite-graph obligation on the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module already has winding kills boundaries and the fundamental loop maps to $1$; what remains is that every free $1$-cycle is an integer combination of cyclic pieces (then directed cycles), so winding is integral and the comparison map is surjective.
Parents: the integral-winding theorem takes this Prop and yields integer winding on all singular $1$-cycles; that feeds the final Mathlib $H_1$ iso and the nonzero $H_1$ target for the linking backend. Sibling bridges turn cyclic edge-list decomposition into abstract directed-cycle decomposition, and close the Prop from extraction-step or large-support hypotheses.
In the Recognition stack this seals the circle homology link used by the Mathlib cohomology bridge, without project-local $S^1$ replacements. It does not itself touch T5–T8 or the RCL; it is pure singular-homology scaffolding for the geometric side of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.