freeBoundaryKernel_decomposesIntoCyclicEdgeLists_of_largeSupport

This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. Together with the fact that the once-around generator has winding $1$, that yields the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The converse (generation) needs a finite decomposition of balanced free $1$-chains into cyclic pieces.

The target proposition says: every free singular $1$-chain $c$ with vanishing free boundary equals a finite list-sum of cyclic singular edge-list terms. The one-step extraction proposition says a nonzero balanced chain can be peeled into one cyclic piece plus a balanced residual of strictly smaller edge-support. Strong induction on support cardinality turns any such one-step extractor into the full finite decomposition.

The remaining open finite-flow input is the large-support case: support cardinality $>1$. Zero, singleton, and loop-edge branches are already closed; the large-support extraction packages exactly that residual case.

One-line term-mode wrapper. First apply the packaging lemma that turns the large-support extraction hypothesis into a full one-step cyclic extraction (it case-splits on support cardinality $\le 1$, discharging the small cases by the already-proved singleton/zero extractor, and hands the $>1$ case to the hypothesis). Then feed that full extraction step into the strong-induction theorem, which builds the finite cyclic edge-list decomposition by induction on edge-support cardinality.

This is the last packaging step before the Mathlib $H_1$ isomorphism for the circle can be stated purely in terms of the genuine remaining finite-flow target. The sole downstream consumer is the final closure theorem: given large-support extraction and a zero-winding filling bound, one obtains the integer comparison isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. That downstream result quotes this lemma explicitly as the bridge from large-support extraction to the abstract cyclic-edge-list decomposition, then composes with the zero-winding bound.

In the module's own terms, this discharges the generation half of the winding homomorphism story: every $1$-cycle becomes homologous to an integer multiple of the fundamental cycle once balanced free flows decompose into cyclic edge lists. No Recognition forcing-chain landmark (T0–T8, RCL, $\varphi$) is directly at stake; the stake is the singular-homology foundation that later geometric arguments sit on. The only remaining scaffold is the large-support extraction hypothesis itself, plus the zero-winding bound.