freeBoundaryKernel_decomposesIntoDirectedCycles_of_cyclicEdgeLists
plain-language theorem explainer
If every free singular 1-cycle on S¹ decomposes into cyclic edge-list pieces, then it also decomposes into abstract directed-cycle pieces. Cited by anyone routing the concrete edge-list target into the directed-cycle winding pipeline. Proof: map each cyclic term to a directed-cycle term and rewrite by the chain-sum preservation lemma.
Claim. Assume that every free singular $1$-chain $c$ with vanishing free boundary admits a finite decomposition into cyclic singular edge-list terms. Then every such $c$ also admits a finite decomposition into directed-cycle free terms.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, the chain-level fact needed for a homology invariant. The long-term goal is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding sends the fundamental loop to $1$ and vanishes on boundaries.
Two Prop-valued targets sit in the free-chain layer. The abstract target says every free $1$-chain in the kernel of the explicit free boundary operator is a finite sum of directed-cycle free terms. The more concrete target says the same chains decompose into cyclic singular edge-list terms (finite closed walks recorded as edge lists).
An upstream equality states that mapping a list of cyclic edge-list terms to directed-cycle terms preserves the represented free-chain sum. That equality is the only algebraic content needed to pass from the concrete Prop to the abstract one.
proof idea
Term-mode implication. Fix a free $1$-chain $c$ with vanishing free boundary. Apply the cyclic-edge-list hypothesis to obtain a list $ts$ of cyclic singular edge-list terms representing $c$. Map each term via the conversion to a directed-cycle free term, and package the image list as the witness. Rewrite the directed-cycle list-chain of that image by the upstream preservation theorem directedCycleListChain_of_cyclicEdgeList, which identifies it with the cyclic edge-list chain of $ts$; the hypothesis equality then closes the goal.
why it matters
This is the one-step bridge from the concrete finite-graph decomposition target to the abstract directed-cycle target used by the winding pipeline. The sole downstream consumer is cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoCyclicEdgeLists, whose doc-comment states that the concrete cyclic edge-list decomposition theorem gives integer winding for all singular $1$-cycles; that theorem simply composes this implication with the directed-cycle integrality route.
In the module's larger program, integer winding on free boundary kernels is the generation/comparison half needed alongside the kills-boundaries identity for the homology isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The present lemma does not discharge the hard decomposition; it only makes the concrete target sufficient for every downstream result already stated against the abstract directed-cycle Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.