largeSupportOrientedScaledExtractionStep_holds
plain-language theorem explainer
Every nonzero balanced free 1-chain on S¹ with support larger than one edge admits an oriented cyclic family that can be scaled by a positive integer so the residual stays balanced and has strictly smaller edge support. Algebraic topologists working the generation half of H₁(S¹;ℤ) ≅ ℤ cite this as the exact finite-flow peel step. The proof extracts a closed oriented walk, scales by the min absolute coefficient, and checks boundary and support bookkeeping.
Claim. For free singular $1$-chains $c$ on $S^1$, if the free boundary of $c$ vanishes, $c \neq 0$, and the edge-support cardinality satisfies $1 < \lvert\mathrm{supp}(c)\rvert$, then there exist an oriented cyclic family term $T$, an integer $m > 0$, and a residual chain $r$ such that $c = r + m \cdot \mathrm{chain}(T)$, the free boundary of $r$ vanishes, and $\lvert\mathrm{supp}(r)\rvert < \lvert\mathrm{supp}(c)\rvert$.
background
This module lifts path-level winding on $S^1$ to singular 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 finite decomposition of balanced free edge-flows into concrete oriented cycles.
A free singular $1$-chain is an integer combination of singular $1$-simplices of $\mathrm{TopCat.sphere},1$. Balance means the free singular boundary map sends it to zero. An oriented cyclic family is a finite injective list of supported edges whose sign-selected orientations connect terminal-to-initial around a cycle; its free chain is the sum of those oriented edge chains.
Upstream, every nonzero balanced flow admits such a family (exists_orientedCyclicFamily_of_balanced_nonzero). Scaling that family by the minimum absolute coefficient on the walk strictly shrinks support (edgeSupportCard_sub_scaled_orientedCyclic_lt), and the cyclic free boundary vanishes by oriented telescoping (cyclicOrientedFamily_freeBoundary_zero).
proof idea
Tactic proof of the Prop interface. From balance and $c \neq 0$, invoke exists_orientedCyclicFamily_of_balanced_nonzero to obtain $k$ and an injective supported family $g$. Build oriented edges by coefficient sign, package them as an OrientedCyclicFamilyTerm $T$ using the cyclic terminal-initial connections, and identify $T$'s chain with orientedCyclicChain c g.
Boundary of $T$ is zero by rewriting to that chain and applying cyclicOrientedFamily_freeBoundary_zero. Support shrinkage supplies $m > 0$ via edgeSupportCard_sub_scaled_orientedCyclic_lt. The residual is $c - m \cdot \mathrm{chain}(T)$; the three goals are the linear identity (abel), residual balance (map_sub, map_zsmul, and the vanishing boundary of $T$), and the strict support inequality already obtained.
why it matters
This discharges the support-cardinality oriented extraction interface used before translating signed oriented cycles into the older one-scalar cyclic edge-list language. The module aims at the generation half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$: every $1$-cycle homologous to an integer multiple of the fundamental cycle. Injectivity already follows from winding killing boundaries plus the once-around generator; surjectivity needs exact finite peels of balanced free flows.
Doc-comment stresses the step is unconditional in substance: the $1 < \mathrm{support}$ hypothesis is kept only to match the large-support interface, while the argument needs only nonzero balanced flow. No downstream consumers are wired yet in the graph; the declaration closes the Prop stub so later induction on support cardinality can peel until the chain is zero or a single-edge cycle.
In the broader Recognition foundation stack this is pure singular-homology infrastructure on $S^1$, not a forcing-chain (T0–T8) step, but it underwrites the circle's integer homology that later winding and octave constructions rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.