largeSupportCyclicEdgeListExtractionStep
plain-language theorem explainer
A balanced nonzero free singular 1-chain on S¹ with support size greater than one splits as one cyclic edge-list term plus a balanced residual of strictly smaller support. Anyone finishing the finite-flow half of H₁(S¹;ℤ) ≅ ℤ cites this Prop as the remaining large-support peel target. It is a pure Prop package: no proof body, only the extraction statement after zero/singleton/loop branches are closed.
Claim. For every free singular $1$-chain $c$ on $S^1$ with $\partial c = 0$, $c \neq 0$, and $|\mathrm{supp}(c)| > 1$, there exist a cyclic singular edge-list term $t$ and a residual free $1$-chain $r$ such that $c = t.\mathrm{chain} + r$, $\partial r = 0$, and $|\mathrm{supp}(r)| < |\mathrm{supp}(c)|$.
background
The 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}$. Generation (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a finite-flow decomposition of the free boundary kernel into cyclic edge-list pieces.
Here singularOneChainFree is the free $\mathbb{Z}$-module on singular $1$-simplices of $\mathrm{TopCat.sphere},1$. The map singularOneBoundaryFree sends each directed edge to terminal $0$-face minus initial $0$-face. Support cardinality edgeSupportCard is the finite cardinality of the Finsupp support of such a chain.
Zero, singleton, and loop-edge extraction branches are already closed. What remains is the large-support case: balanced nonzero flows with more than one supported edge.
proof idea
No proof: this is a Prop definition. It asserts existence of a cyclic singular edge-list term $t$ and residual $r$ with $c = t.\mathrm{chain} + r$, residual still in the free boundary kernel, and strict drop of support cardinality.
Downstream discharge routes package stronger peels into this target: supported exact cyclic peel (via edgeSupportCard_sub_lt_of_supported_exact_cancel), or uniform-oriented (forward/backward) extraction. The definition itself only names the residual-support drop that induction needs.
why it matters
This is the single remaining finite-flow input after small-support cases close. Feeding it yields cyclicEdgeListExtractionStep_of_largeSupport, then freeBoundaryKernel_decomposesIntoCyclicEdgeLists_of_largeSupport, and finally circleH1ZIsoInt_of_largeSupport_of_zeroWinding_bounds (and the nonzero $H_1$ backend). Downstream docs call it "the exact remaining finite-flow target" and "the only finite-flow input" once zero-winding filling is assumed.
In the module arc it completes the generation half of the integer comparison $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ that Mathlib singular homology does not yet supply via prism/subdivision. It is scaffolding for the circle linking backend, not a physics constant claim; the eight-tick and $D=3$ landmarks sit upstream in the forcing chain, not here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.