orientedCyclicFamilyTermList_boundary_generates
plain-language theorem explainer
If every oriented cyclic family on S¹ is homologous to an integer multiple of the fundamental cycle, then the same holds for any finite list of such families. Cited when lifting the local geometric generation hypothesis to finite sums of closed walks in the singular chain complex. The proof is induction on the list, adding the integer coefficients and 2-chains and using additivity of the cycle maps.
Claim. Assume that for every concrete oriented cyclic family $T$ (a finite sign-oriented closed walk in singular $1$-simplices of $S^1$) there exist $n\in\mathbb{Z}$ and a singular $2$-chain $b$ such that the cycle of $T$ equals $\partial b + n\,[S^1]$. Then for every finite list $ts$ of such families there exist $n\in\mathbb{Z}$ and a $2$-chain $b$ with the same relation for the sum of the cycles of the list.
background
This module lifts path-level winding 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}$. The generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) is still open at the full chain level and is approached here via concrete closed walks.
An oriented cyclic family is a finite sign-oriented closed walk in singular $1$-simplices: $k$ oriented edges with matching terminals and initials under cyclic rotation. Each such family packages to a directed-cycle-free term whose cycle lives in degree $1$ of the integer singular chain complex of $\mathrm{TopCat.sphere},1$. Lists of families sum those cycles.
The hypothesis orientedCyclicFamilies_boundary_generate asserts the local geometric target: every single family is homologous to $n$ times the fundamental cycle (the once-around generator lifted to a cycle object) plus a boundary from degree $2$. The fundamental cycle is the lift of the standard once-around singular $1$-chain via the zero-boundary proof.
proof idea
Induction on the list of oriented cyclic family terms, under the standing hypothesis that every single family is generated modulo boundary.
Empty list: take $n=0$ and $b=0$; both the list-cycle and the right-hand side unfold to zero.
Cons step: apply the hypothesis to the head term $T$ to obtain $n_1,b_1$, and the inductive hypothesis to the tail to obtain $n_2,b_2$. Set $n=n_1+n_2$ and $b=b_1+b_2$. Rewrite the list-cycle as head cycle plus tail cycle, substitute the two generation equalities, push addition through the boundary map and through the fundamental-cycle map, and finish by abelian cancellation.
why it matters
This is the finite-sum bridge from the local geometric generation hypothesis to the global chain-level generation theorem. Downstream, fundamentalCycle_boundary_generates_of_orientedCyclicFamilies quotes it to conclude that every singular $1$-cycle is homologous to an integer multiple of the fundamental cycle once every concrete oriented cyclic family is so generated.
In the module's program that is the missing surjectivity half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, complementary to the winding homomorphism that already splits the fundamental class. Within Recognition Science this feeds the strict T8 target: the integer homology of the circle as the chain-level witness for the forced spatial dimension and the eight-tick octave structure built on $S^1$ windings. The declaration itself is fully proved; it only packages the list extension once the per-family geometric work is supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.