directedCycleFreeTermList_chain_eq
plain-language theorem explainer
For any finite list of directed-cycle free terms, the free-chain image of their summed cycle object equals the explicit free-chain sum of the pieces. Anyone assembling multi-edge cycle decompositions of singular 1-cycles on S¹ cites this. The proof is list induction: empty case by unfolding, cons case by additivity of the free map plus each term’s built-in chain_eq.
Claim. For every finite list $ts$ of directed-cycle free terms (each pairing a singular $1$-cycle on $S^1$ with an explicit free $1$-chain and a witness that the free-chain map sends the cycle to that chain), the free-chain image of the summed cycle object of $ts$ equals the summed free chain of $ts$.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries, giving the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) is still open and is attacked via free-chain decompositions.
A DirectedCycleFreeTerm packages one directed multi-edge cycle piece: a degree-$1$ cycle in the integer singular chain complex of $\mathrm{TopCat.sphere},1$, an explicit free $1$-chain, and the equality that the free-chain map (composed with the cycles inclusion) recovers that chain, plus an integrality witness for winding.
List-level sums are defined recursively: the cycle-object sum and the free-chain sum of a list. The singular complex is Mathlib’s integer singular chain complex of $S^1$; the free map is the comparison from singular chains into free-edge coordinates used throughout the generation argument.
proof idea
List induction on $ts$.
Empty list: unfold both list-sum definitions and simplify; both sides are zero.
Cons $t::ts$: unfold the recursive sums, rewrite with additivity of the free-chain map (twice, once for the cycles inclusion composite), apply the term’s own chain_eq field on $t$, then invoke the inductive hypothesis on the tail. No extra geometric input.
why it matters
This is the bookkeeping bridge that lets list-level directed-cycle decompositions pass between cycle-object and free-chain coordinates without losing equality. Downstream, cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoDirectedCycles uses it so that a free-boundary-kernel decomposition into directed cycles implies integer winding for every singular $1$-cycle. The generation targets fundamentalCycle_boundary_generates_of_directedCycleTerms and fundamentalCycle_boundary_generates_of_orientedCyclicFamilies likewise reduce global chain-level generation to filling individual directed pieces, and need the free image of the list-sum to match the explicit free sum.
In the module’s program this supports the missing surjective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (the injective half already comes from winding). Framework-wise it sits under the T8 spatial-dimension / circle homology infrastructure rather than the J-cost or phi-ladder layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.