freeBoundaryKernel_decomposesIntoCyclicEdgeLists_of_extractionStep
plain-language theorem explainer
A one-step support-decreasing cyclic extraction of balanced free edge-flows yields the full finite cyclic edge-list decomposition of the free boundary kernel. Anyone closing the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via singular chains would cite this reduction. The argument is strong induction on edge-support cardinality: peel one cyclic piece, apply the inductive hypothesis to the residual.
Claim. Assume every nonzero free singular $1$-chain $c$ with vanishing free boundary splits as $c=t+r$, where $t$ is one cyclic edge-list term and the residual $r$ is again free-boundary-zero with strictly smaller edge support. Then every free-boundary-zero free $1$-chain equals a finite sum of cyclic edge-list terms.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half needs a concrete description of free $1$-cycles: every free-boundary-zero free edge-flow should be a finite integer combination of cyclic edge walks.
The free boundary map singularOneBoundaryFree is the singular boundary on free $1$-chains. Its kernel is the free boundary kernel. Edge support cardinality counts how many distinct singular edges appear with nonzero coefficient. A cyclic edge-list term packages one closed edge walk with an integer coefficient; summing a finite list of such terms recovers a free chain.
The one-step extraction hypothesis states that every nonzero balanced free edge-flow splits into one cyclic piece plus a balanced residual of strictly smaller support. That is the inductive engine; this theorem turns the engine into the full decomposition.
proof idea
Define a predicate $P(n)$: every free chain of edge-support size $n$ with vanishing free boundary is a finite cyclic edge-list sum. Prove $P(n)$ for all $n$ by strong induction on $n$.
For a chain $c$ of support $n$: if $c=0$, take the empty list. Otherwise apply the extraction step to obtain a cyclic term $t$ and residual $r$ with free boundary zero and strictly smaller support. The inductive hypothesis decomposes $r$ as a list ts; cons $t$ onto ts and unwind the list-sum definition to match $c=t+r$.
Instantiate at $n$ equal to the support of the input chain.
why it matters
This is the induction bridge from a local extraction step to global generation of free $1$-cycles by cyclic edge lists. Downstream, circleH1ZIsoInt_of_extractionStep_of_zeroWinding_bounds feeds the conclusion (with a zero-winding filling bound) into the Mathlib $H_1$ comparison isomorphism: "Final Mathlib $H_1$ closure from the support-decreasing cyclic extraction step and filling of zero-winding cycles."
A sibling path specializes the step via large-support repeated-vertex extraction and reuses this theorem. In the module's program, winding already kills boundaries and hits the fundamental loop; the missing surjectivity half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is exactly finite generation of cycles by cyclic walks, which this reduction isolates. No Recognition forcing-chain step (T0–T8) is invoked here; the result is pure singular-homology scaffolding for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.