cyclicEdgeListExtractionStep
plain-language theorem explainer
Every nonzero balanced free singular 1-chain on S¹ factors as one cyclic edge-list piece plus a balanced residual of strictly smaller edge support. This Prop is the one-step extraction target for support induction toward H₁(S¹;ℤ) ≅ ℤ. Algebraic topologists closing the generation half of the integer comparison map cite it. Pure definition of a proposition; no proof content.
Claim. The assertion that for every free singular $1$-chain $c$ on $S^1$ with vanishing free boundary and $c \neq 0$, there exist a cyclic singular edge-list term $t$ and a residual free $1$-chain $r$ such that $c = t.(\mathrm{chain}) + r$, the free boundary of $r$ vanishes, and the edge-support cardinality of $r$ is strictly smaller than that of $c$.
background
The module works at the level of singular simplices of the topological circle $S^1 = \mathrm{TopCat.sphere},1$. Free singular $1$-chains are the free $\mathbb{Z}$-module on actual singular $1$-simplices. The free boundary sends each directed edge to its terminal $0$-face minus its initial $0$-face; a chain is balanced when that boundary vanishes (a free $1$-cycle).
Edge-support cardinality is the finite cardinality of the support of such a free chain; it is zero exactly on the zero chain. A cyclic singular edge-list term packages one closed walk of edges as a free chain summand. The module already has the winding/displacement invariant on singular $1$-simplices and the kills-boundaries identity (alternating face displacements of any $2$-simplex sum to zero), giving the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. Generation (every free $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a finite decomposition of balanced free edge-flows into cyclic pieces.
proof idea
No proof: this is a bare Prop definition. The body is the universal quantification over free $1$-chains of the one-step split (cyclic term plus balanced residual with strictly smaller edge support). Downstream, strong induction on support cardinality consumes an assumption of this Prop; the support-$\le 1$ base cases are handled separately, and the large-support case is the remaining obligation.
why it matters
This is the single inductive step hypothesis that turns finite support decrease into a full cyclic edge-list decomposition of the free boundary kernel. The immediate parent is freeBoundaryKernel_decomposesIntoCyclicEdgeLists_of_extractionStep, which runs strong induction on edge-support cardinality from this step. That decomposition, paired with zero-winding cycle filling, yields the Mathlib $H_1$ isomorphism to $\mathbb{Z}$, the nonzero $H_1$ witness, and the Mathlib circle-linking backend required by the strict T8 replacement (forcing $D=3$).
In the module narrative, injectivity of winding is already closed; this Prop is the generation-side hinge. The large-support reduction packages the remaining work so only repeated-vertex extraction for support $>1$ must still be proved. Framework landmark: closes the surjectivity half of the integer comparison map that underwrites the circle-linking backend in the T8 spatial-dimension chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.