directedCycleFreeTermList_boundary_generates
plain-language theorem explainer
If each directed-cycle free term on S¹ is homologous to an integer multiple of the fundamental cycle, then the same holds for every finite list of such terms. Homology generators for H₁(S¹;ℤ) cite this when lifting single-walk generation to multi-component edge flows. The proof is list induction: empty list is zero; cons adds the two witnesses and uses additivity of the cycle sum and boundary map.
Claim. Assume that for every directed-cycle free term $t$ there exist $n\in\mathbb{Z}$ and a singular $2$-chain $b$ with $t.\mathrm{cycle}=\partial b+n\,[S^1]$. Then for every finite list $ts$ of such terms there exist $n\in\mathbb{Z}$ and a singular $2$-chain $b$ such that the sum of the cycles in $ts$ equals $\partial b+n\,[S^1]$ in the degree-$1$ cycles of the singular chain complex of $S^1$ with integer coefficients.
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 remaining generation half needs every $1$-cycle homologous to an integer multiple of the fundamental cycle.
A DirectedCycleFreeTerm packages a degree-$1$ cycle together with a free edge-chain presentation and an integrality witness for its winding. The list sum directedCycleFreeTermListCycle adds those cycle objects. The hypothesis directedCycleTerms_boundary_generate asserts the single-term statement: each such cycle equals a boundary plus an integer multiple of fundamentalCycle (the once-around generator lifted to the cycle object of Mathlib's singular chain complex of TopCat.sphere 1).
This lemma is the purely formal extension from one term to a finite list, before the global generation theorem is assembled.
proof idea
Proof by induction on the list, under the standing hypothesis that every single term is boundary-generated.
Empty list: take $n=0$ and $b=0$; the list-cycle definition unfolds to $0$, and both sides match by simplification.
Cons case $t::ts$: apply the hypothesis to $t$ to obtain $(n_1,b_1)$; recurse on $ts$ to obtain $(n_2,b_2)$. Return $(n_1+n_2,,b_1+b_2)$. Unfold the list-cycle sum, rewrite by the two witnesses, push addition through the boundary map and through fundamentalCycle via map_add, then finish by abelian-group cancellation (abel).
why it matters
Feeds directly into fundamentalCycle_boundary_generates_of_directedCycleTerms, whose doc-comment states that boundary-generation for individual directed-cycle terms implies the global circle chain-level generation theorem. Combined with the equivalence zeroWindingCycles_bound_iff_fundamentalCycle_boundary_generates, that parent is the next minimal geometric target: fill one directed closed walk.
In the Recognition foundation stack this is part of the strict computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, the homology side of the T8 / circle story (once-around generator, winding as left inverse). The module already has the kills-boundaries identity; generation is the missing surjectivity half. This lemma removes the bookkeeping gap between single directed-cycle pieces and finite multi-component flows, so the remaining work is geometric (construct the $2$-chain for one closed directed walk) rather than formal list algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.