edgeCoeff_sub

This module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$, and proves that simplex displacement kills boundaries. Free singular $1$-chains are the free $\mathbb{Z}$-module on actual singular $1$-simplices; the edge coefficient of a chain at a simplex is simply the value of the underlying finitely supported function.

The local goal is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding on $1$-cycles is a left inverse to the fundamental class. Generation (every cycle homologous to an integer multiple of the fundamental cycle) needs support bookkeeping for cyclic extraction, which repeatedly subtracts oriented closed walks from balanced flows.

Linearity of coefficients under subtraction is the elementary algebraic step those support and $\ell^1$ identities rest on.

Unfold the coefficient map to evaluation of the underlying finitely supported function. The claim is then exactly Finsupp.sub_apply on the two chains at the given simplex: a one-line term proof, no further lemmas.

This is the coefficient-level subtraction rule used throughout cyclic peel arguments in the circle winding chain. Downstream it feeds the $\ell^1$ decrease of one directed-cycle peel (subtracting an oriented closed walk of $k$ supported edges lowers $\ell^1$ size by exactly $k$), the generic support-cardinality shrinkage when a supported peel exactly cancels at least one edge, and the coefficient and support identities for two-edge parallel flows.

Those facts are the bookkeeping half of one-step cyclic extraction toward the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module already has the kills-boundaries identity and the winding of the fundamental loop; what remains is surjectivity of the integer comparison map via simplicial prism or subdivision (not yet in Mathlib singular homology). No Recognition forcing-chain step (T0–T8) is touched directly; the result is pure singular-chain algebra on $S^1$.