largeSupportOrientedScaledExtractionStep
plain-language theorem explainer
Any nonzero balanced free singular 1-chain on S¹ whose edge support has size greater than one can be written as a positive integer multiple of an oriented closed-walk chain plus a residual balanced chain of strictly smaller support. Anyone decomposing singular 1-cycles into oriented cyclic pieces before the one-scalar edge-list interface cites this statement. It is packaged as a Prop; the companion theorem discharges it from existence of an oriented cyclic family on nonzero balanced flow.
Claim. For every free singular $1$-chain $c$ on $S^1$ with vanishing boundary, $c\neq 0$, and edge-support cardinality strictly greater than $1$, there exist an oriented cyclic-family term $T$, a positive integer $m>0$, and a residual free $1$-chain $r$ such that $c=m\cdot(\text{chain of }T)+r$, the residual $r$ has vanishing boundary, and the edge-support cardinality of $r$ is strictly smaller than that of $c$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$ and proves the kills-boundaries identity that makes winding a homology invariant. Together with the fact that the once-around generator has winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; the generation half needs finite-flow extraction of cycles from balanced chains.
Here a free singular $1$-chain is an element of the free $\mathbb{Z}$-module on singular $1$-simplices of $\mathrm{TopCat.sphere},1$. Its boundary map sends each directed edge to terminal $0$-face minus initial $0$-face. Edge-support cardinality is the finite cardinality of the Finsupp support. Balanced means boundary zero (closed integer flow on the $1$-skeleton).
The statement is the support-cardinality form of oriented extraction: peel a positively scaled oriented closed walk so the residual stays balanced and has strictly smaller support. The module doc positions this as the exact finite-flow step needed before translating signed oriented cycles into the older one-scalar cyclic edge-list interface.
proof idea
This declaration is a bare Prop definition: its body is the universal quantifier over free $1$-chains, boundary vanishing, nonzeroness, and support size $>1$, asserting existence of an oriented cyclic-family term $T$, scale $m>0$, and residual $r$ with the four listed properties. There is no proof obligation on the def itself.
The companion theorem that asserts the Prop holds proceeds by introducing $c$ with boundary zero and $c\neq 0$, ignoring the large-support hypothesis beyond interface matching, and invoking existence of an oriented cyclic family on any nonzero balanced free chain. From that family one scales by the minimum absolute coefficient along the walk and forms the residual; balance of the residual and strict drop in support cardinality are then immediate from the family construction.
why it matters
The sole downstream consumer is the theorem that the support-cardinality oriented extraction step holds unconditionally: the $1<\mathrm{support}$ hypothesis is kept only to match the large-support interface, while the proof needs only nonzero balanced flow. That theorem is the certified finite-flow engine for decomposing singular $1$-cycles on $S^1$.
In the module narrative this sits on the generation side of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: after winding kills boundaries and hits the fundamental class by $1$, one still needs every balanced free $1$-chain to reduce, by repeated extraction, to an integer multiple of a fundamental cycle. The doc-comment states this is the exact finite-flow theorem required before translating signed oriented cycles into the older one-scalar cyclic edge-list term. It does not itself close the Mathlib gap on simplicial prisms or subdivision operators, but it supplies the combinatorial peeling step those arguments would feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.