cyclicSingularEdgeListTermListChain_single
plain-language theorem explainer
A singleton list of concrete cyclic edge-list terms represents, as a free 1-chain on S¹, exactly the chain already stored on that term. Anyone assembling multi-piece cycle decompositions into free chains cites this base case. The proof is a one-line simp unfolding the recursive list-sum definition against the term's chain field.
Claim. For every concrete cyclic edge-list term $t$ (a finite list of singular $1$-simplices with integer coefficient and a certified cycle whose free-chain image is that coefficient times the edge sum), the free-chain sum of the singleton list $[t]$ equals the free chain carried by $t$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that displacement kills boundaries of singular $2$-simplices. That identity, with the generator evaluation on the fundamental loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A CyclicSingularEdgeListTerm packages a finite list of singular $1$-simplices, a global integer coefficient, a certified $1$-cycle, and the equality that the free-chain image of that cycle is the coefficient times the listed edge sum (plus an integrality witness for the winding). The list-level free-chain sum is defined recursively: empty list maps to $0$; a cons cell adds coeff times the edge-list chain of the head to the sum of the tail.
The present lemma is the singleton base case of that recursion: the free chain of $[t]$ is just the chain already attached to $t$.
proof idea
One-line simp against the recursive definition of the list free-chain sum and the term's chain field. Unfolding the cons/nil clauses on the singleton list reduces the left-hand side to the coefficient-scaled edge-list chain of $t$, which is definitionally the term's chain.
why it matters
In the CircleWindingChain development this is bookkeeping infrastructure for free-chain sums of concrete cyclic edge-list pieces. Those sums feed the comparison between listed edge cycles and abstract directed-cycle terms, which in turn support the winding homomorphism on $1$-cycles as a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ from the module header).
No downstream consumers are recorded yet; the lemma is a local algebraic identity rather than a forcing-chain (T0–T8) step. It does not touch RCL, $\varphi$, or the eight-tick octave. It closes a trivial but necessary base case so multi-term list identities can be stated cleanly without re-unfolding the recursion at every use site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.