edgeCoeff_singularEdgeListChain_nonneg
plain-language theorem explainer
Any finite forward list of singular 1-simplices on S¹ yields a free C₁ chain whose coefficient at every singular edge is a nonnegative integer. Cited when packaging listed edge-sums into cyclic edge-list terms before a global integer scalar is applied. Proof is list induction with a head-equality case split on the coefficient lemmas.
Claim. Let $es$ be a finite list of singular $1$-simplices on $S^1$, and let $e$ be any singular $1$-simplex. Writing $c(es)$ for the free $C_1$ chain that is the sum of the free generators of the entries of $es$ (each with coefficient $1$), the coefficient of $e$ in $c(es)$ satisfies $0 \le [c(es):e]$ in $\mathbb{Z}$.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $\mathrm{TopCat.sphere},1$, and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is an element of the degree-$1$ object of the singular simplicial set of $S^1$. The free $C_1$ module is the explicit free $\mathbb{Z}$-module on those simplices; edgeCoeff reads the integer coefficient of a chosen edge in such a free chain. The list-to-chain map singularEdgeListChain sends a finite list to the sum of free generators of its entries (empty list to $0$, cons by free generator plus recursive tail).
Upstream coefficient facts used here: coefficients are additive under chain sum; a free generator has coefficient $1$ on itself; a Finsupp singleton has the written value at its support point and $0$ elsewhere.
proof idea
List induction on $es$.
Nil: unfold the list-to-chain map and the coefficient extractor; both sides are $0$, so reflexivity.
Cons $a::as$: unfold the list-to-chain map to free generator of $a$ plus the tail chain, then rewrite by coefficient additivity. Case on $a=e$. If equal, substitute and apply the free-generator self-coefficient lemma (value $1$), then omega gives nonnegativity of $1$ plus the inductive hypothesis. If unequal, the free-generator coefficient at $e$ is $0$ by the singleton-coefficient lemma with the negative branch of the equality test; rewrite and again omega with the inductive hypothesis.
why it matters
The nonnegativity fact is the coefficient hygiene needed before a global integer scalar is applied to a listed edge sum. Downstream it is consumed by the structure CyclicSingularEdgeListTerm, which packages a concrete finite list of singular $1$-simplices, a global integer coefficient, a certified $1$-cycle, and the equality that the cycle's free-chain image is that scalar times the listed edge sum, together with an integrality witness for the cycle winding.
In the module's larger program this sits under the winding-kills-boundaries identity and the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (winding sends the once-around generator to $1$). It does not touch the still-open generation/surjectivity half, which needs a simplicial prism or subdivision operator Mathlib's singular homology does not yet supply. No Recognition forcing-chain landmark (T5–T8, RCL, phi) is directly at stake; the result is pure singular-homology bookkeeping on $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.