cyclicSingularEdgeListTerm_of_loop
plain-language theorem explainer
A closed singular 1-simplex on S¹, scaled by an integer coefficient, is packaged as a cyclic edge-list term with singleton edge list. Anyone running the finite-flow extraction (support-decreasing peel of balanced free 1-chains) cites this for the loop-edge base case. The construction feeds the closed singular generator into the cycle object and checks the free-chain and integral-winding fields by the closed-simplex identities already proved upstream.
Claim. Given a singular $1$-simplex $e$ on $S^1$ whose two face maps agree (equal endpoints) and an integer coefficient $n$, there is a cyclic edge-list term whose edge list is $[e]$, coefficient is $n$, underlying cycle is $n$ times the closed singular generator of $e$, free-chain image equals $n$ times the listed edge sum, and cycle winding is an integer.
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries of $2$-simplices, so winding descends to a homology invariant. Together with the once-around generator mapping to $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The remaining generation half needs every balanced free $1$-chain decomposed into cyclic edge-list pieces.
A CyclicSingularEdgeListTerm records a finite list of singular $1$-simplices, a global integer coefficient, a certified degree-$1$ cycle whose free-chain image is that coefficient times the listed edge sum, and a witness that cycle winding is integral. A singular $1$-simplex is closed when its two face maps $\delta_0$ and $\delta_1$ agree.
Upstream, closedSingularOneCycle builds the cycle object from such a closed simplex; closedSingularOneCycle_iCycles says including it into $C_1$ recovers the coproduct generator; cycleWinding_closedSingularOneCycle multiplies the simplex winding by the coefficient.
proof idea
Structure constructor. Edge list is the singleton $[e]$; coefficient is the given $n$; cycle is the image of $n$ under the closed singular generator morphism.
For chain_eq: postcompose the identity closedSingularOneCycle_iCycles with the free-chain map, rewrite the composite, apply the coproduct-inclusion formula for free chains, and simplify the singleton edge-list chain to $n$ times the generator.
For winding_integral: invoke integrality of winding on a closed singular loop, scale by $n$ via cycleWinding_closedSingularOneCycle, and simplify.
why it matters
This is the loop-edge base case of finite-flow extraction on balanced free $1$-chains in the singular complex of $S^1$. When the selected supported edge is already closed, no successor walk is required: the edge itself is a cyclic term.
Downstream, singleEdgeFlow_decomposesIntoCyclicEdgeLists uses it for support-cardinality one; supportCard_le_one_extractionStep packages that into the one-step extraction interface; loopEdge_plus_residual_decomposesIntoCyclicEdgeLists peels a loop edge and reattaches a residual decomposition. Those feed the support-decreasing extraction that aims at the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (the surjectivity gap left after the kills-boundaries identity).
In the broader Recognition chain this is foundation scaffolding for the circle homology computation that underwrites the eight-tick / $D=3$ forcing landmarks, not a physics identity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.