edgeCoeff_orientedCyclicChain
plain-language theorem explainer
For an oriented closed walk built from a free 1-chain flow c and an injective family of k edges, the coefficient at any edge e is the sign-unit of c on the walk and zero off it. Cycle-peel and ℓ¹ bookkeeping lemmas cite this as the pointwise evaluation of the peeled walk. The proof unfolds the walk as a sum of signed generators, evaluates each term, and collapses the sum by injectivity.
Claim. Let $c$ be a free singular $1$-chain on $S^1$, and let $g:\mathrm{Fin}\,k\to\{\text{singular $1$-simplices}\}$ be injective. Write $P$ for the oriented closed-walk chain obtained by summing, over $i$, the generator for $g(i)$ with coefficient $+1$ or $-1$ according to the sign of $c$ at $g(i)$. Then for every edge $e$, the coefficient of $P$ at $e$ equals $+1$ if $e$ lies in the image of $g$ and $c(e)>0$, equals $-1$ if $e$ lies in the image and $c(e)\le 0$, and equals $0$ otherwise.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Free $1$-chains are explicit Finsupp modules on singular $1$-simplices of $\mathrm{TopCat.sphere},1$; edgeCoeff is pointwise evaluation of that Finsupp.
An oriented edge of a flow pairs a simplex with the forward/backward orientation of the sign of its coefficient. The free-chain contribution of one such oriented edge is the single generator with coefficient $+1$ or $-1$ (orientedEdgeOfCoeff_chain_eq_single). An oriented closed walk through an injective family $g$ is the sum of those contributions (orientedCyclicChain).
The local goal is exact coefficient control for cycle peeling: once coefficients of the walk are known pointwise, support, $\ell^1$ mass, and strict support decrease after subtraction become elementary Finset arithmetic.
proof idea
Unfold the definition of the oriented closed walk as $\sum_i$ of oriented-edge chains. Apply coefficient-of-sum to push edgeCoeff inside the finite sum. For each index $i$, rewrite the $i$-th term via orientedEdgeOfCoeff_chain_eq_single and evaluate with edgeCoeff_single, obtaining the indicator that $g(i)=e$ times the sign-unit of $c$ at $g(i)$. Congruence of the sum, then the lemma that sums of if-selected values over an injective family collapse to a single image membership test, yields the claimed piecewise formula.
why it matters
This is the pointwise engine under the cycle-peel calculus in CircleWindingChain. Immediately downstream, edgeSupport_orientedCyclicChain reads off that the walk's support is exactly the image of $g$; chainL1_orientedCyclicChain then gets $\ell^1(P)=k$. The decrease identities chainL1_sub_orientedCyclic, edgeSupportCard_sub_orientedCyclic_lt_of_unitCoeff, and edgeSupportCard_sub_scaled_orientedCyclic_lt all rewrite coefficients after subtracting (a multiple of) the walk and need this evaluation to show magnitudes drop by one on the walk and support strictly shrinks when a unit or min-coefficient edge is hit.
In the broader module story, those peels are the combinatorial half of showing every $1$-cycle is homologous to an integer multiple of the fundamental loop (the generation/surjectivity direction toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). The winding/kills-boundaries half is already settled by simplexDisplacement_boundary; this lemma is pure free-chain bookkeeping that makes the peel well-defined and measure-decreasing. No Recognition forcing landmark (T5–T8, RCL) is invoked here: the result is singular-homology infrastructure on $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.