directedCycleFreeTermListCycle
plain-language theorem explainer
Sums a finite list of directed-cycle free terms into a single singular 1-cycle on S¹ by adding their cycle components. Algebraic topology and RS circle-homology arguments cite it whenever a balanced edge flow is decomposed into directed cycles and those pieces must be reassembled as one homology class. The body is a recursive list fold: empty list to zero, cons to cycle-sum.
Claim. Given a finite list of directed-cycle free terms (each carrying a singular $1$-cycle on $S^1$ together with a free-chain representative), form the singular $1$-cycle obtained by summing the cycle components of the list entries; the empty list maps to the zero cycle.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, so winding descends to a homology invariant on $H_1(S^1;\mathbb{Z})$. The ambient chain object is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients, whose degree-$1$ cycles are the codomain here.
A directed-cycle free term packages one such $1$-cycle together with its image in free edge-chain coordinates, the equality relating the two, and the existence of an integer winding number. Unlike a single closed singular edge, a term may encode a multi-edge directed cycle, exactly the data a finite-graph cycle decomposition produces from a balanced edge flow.
This definition is the list-level assembly map: it turns a finite collection of those pieces into one cycle object so that free-chain images, winding integrals, and boundary-generation statements can be stated uniformly for decompositions rather than single terms.
proof idea
Definition by structural recursion on the list. The empty list is the zero cycle in degree $1$. On a cons cell, add the head term's stored cycle field to the recursively computed sum of the tail. No lemmas are invoked; the construction is the additive monoid structure on the module of $1$-cycles.
why it matters
This is the bookkeeping glue between single directed-cycle pieces and global statements about all singular $1$-cycles. Downstream it feeds the free-chain image identity for lists, the theorem that every finite directed-cycle list has integer winding, and the lift of termwise boundary-generation to listwise boundary-generation.
Those list facts are then used to pass from a kernel-decomposition hypothesis (every free boundary-kernel class splits into directed cycles) to integer winding for arbitrary cycles, and from termwise generation by the fundamental cycle to the global generation theorem for $H_1(S^1;\mathbb{Z})$. In the module narrative that generation half is the missing surjectivity side of the comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, complementary to the already-proved winding left-inverse on the fundamental loop. Oriented cyclic-family list variants reuse the same pattern.
Within Recognition Science this sits in the Foundation circle-homology chain aimed at the strict T8 target (three spatial dimensions via the circle's first homology), not at the J-cost or phi-ladder layer directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.