loopEdge_plus_residual_decomposesIntoCyclicEdgeLists
plain-language theorem explainer
If a singular 1-simplex on S¹ is a loop edge (matching endpoints) and the residual free 1-chain is already a finite sum of cyclic edge-list pieces, then any integer multiple of that edge plus the residual remains such a sum. Finite-flow extraction on the circle cites this as the closed loop-edge branch. The proof prepends the canonical loop term and rewrites the free-chain recursion.
Claim. Let $e$ be a singular $1$-simplex on $S^1$ whose two face maps agree (a loop edge), let $n\in\mathbb{Z}$, and let $r$ be a free singular $1$-chain equal to the free-chain image of a finite list of cyclic edge-list terms. Then $n\cdot[e]+r$ equals the free-chain image of some finite list of cyclic edge-list terms.
background
The ambient module lifts path-level winding on the circle to singular simplices of TopCat.sphere 1 and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is a point of the singular simplicial set in degree $1$. The free $\mathbb{Z}$-module on those simplices is the ambient chain group. A cyclic edge-list term packages a finite list of singular edges, an integer coefficient, a certified $1$-cycle, and the equality that the cycle's free image is that coefficient times the listed edge sum (plus an integrality witness for winding). The free-chain sum of a list of such terms is the recursive head-tail sum of those scaled edge-list chains.
Upstream, a single edge with $\delta_0 e=\delta_1 e$ is already a cyclic edge-list term for any integer coefficient: no successor search is required. The residual hypothesis says the leftover chain is already a list-sum of such terms.
proof idea
Unpack the residual witness list. Build the loop term from the given edge, face-agreement hypothesis, and integer coefficient via the loop-edge constructor. Take the cons of that term onto the residual list as the new witness. Unfold the list-to-chain recursion, rewrite by the residual equality, and simplify so the head contribution is exactly the scaled free generator of the loop edge plus the residual chain.
why it matters
Generation of $H_1(S^1;\mathbb{Z})$ needs a combinatorial extraction that peels any balanced finite $1$-flow into cyclic edge-list pieces. The doc-comment places this lemma as the loop-edge branch of the future support-decreasing extraction proof: once zero, singleton, and loop-edge cases close, the remaining target is a balanced nonzero flow of support cardinality greater than one, split into one cyclic piece plus a strictly smaller balanced residual.
No downstream uses are wired yet; the declaration is pure infrastructure for that extraction. In the broader foundation stack it feeds the singular comparison that makes winding a homology invariant on the circle, adjacent to the eight-tick octave and circle geometry used elsewhere in the forcing chain. It does not by itself finish surjectivity of the integer comparison map (that still needs prism/subdivision technology Mathlib lacks).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.