directedCycleListChain_of_cyclicEdgeList
plain-language theorem explainer
Mapping a finite list of concrete cyclic edge-list pieces to abstract directed-cycle terms preserves the free $C_1$ chain they represent. Anyone proving that free-boundary-kernel classes decompose into directed cycles cites this bridge. The argument is structural induction on the list: the empty case is definitional equality, and the cons case unfolds both recursive sums and applies the inductive hypothesis.
Claim. For every finite list $ts$ of concrete cyclic edge-list terms (each a finite list of singular $1$-simplices with an integer coefficient and a certified cycle whose free-chain image is that coefficient times the edge sum), the free $C_1$ chain of the mapped abstract directed-cycle terms equals the free-chain sum built directly from the cyclic edge-list data.
background
This module lifts the path-level winding/displacement invariant 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}$.
A concrete cyclic edge-list term packages a finite list of singular $1$-simplices, a global integer coefficient, and a certified $1$-cycle whose image under the free-chain map is that coefficient times the listed edge sum (with an integrality side condition on winding). The free-chain sum of such a list is defined recursively: zero on the empty list, and coefficient times the edge-list chain plus the tail sum on a cons cell. Parallel to that, directed-cycle free terms have their own recursive free-chain sum (term chain plus tail).
The conversion toDirectedCycleFreeTerm turns each concrete cyclic piece into an abstract directed-cycle piece. This lemma says the two free-chain accumulators agree after that conversion.
proof idea
Structural induction on the list of cyclic edge-list terms.
Empty list: unfold both free-chain accumulators; both are definitionally $0$, so rfl closes.
Cons cell $t::ts$: unfold both accumulators. The goal becomes equality of $t.\mathrm{coeff}\cdot(\text{edge-list chain of }t)$ plus the recursive free-chain of the mapped tail, versus the same head summand plus the cyclic free-chain of the tail. Rewrite by the inductive hypothesis on $ts$; the two sides match.
why it matters
This is the bookkeeping bridge from concrete cyclic edge-list data to the abstract directed-cycle language used in the free-boundary-kernel decomposition target. The sole downstream consumer is freeBoundaryKernel_decomposesIntoDirectedCycles_of_cyclicEdgeLists, whose doc-comment states: concrete cyclic edge-list decomposition implies the abstract directed-cycle decomposition target. That theorem maps a witnessing list through toDirectedCycleFreeTerm and needs exactly this chain-sum identity to finish.
In the broader module arc, the winding invariant on singular $1$-simplices plus the kills-boundaries identity give the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The remaining generation half (every free $1$-cycle homologous to an integer multiple of the fundamental cycle) is approached by decomposing balanced free edge-flows into finitely many cyclic pieces; this lemma keeps the concrete and abstract presentations interchangeable along that path. It does not itself touch T0–T8 or the RCL; it is pure singular-chain bookkeeping inside the circle homology forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.