sum_ite_image_of_injective
plain-language theorem explainer
Over an injective finite family of singular 1-simplices, the sum of if-selected integer values collapses to F(e) when the test edge e lies in the image, and to 0 otherwise. Anyone extracting pointwise coefficients of free edge-chains from oriented closed walks cites this. The proof is a membership case-split plus single-term reduction of the sum via injectivity.
Claim. Let $S$ be the set of singular $1$-simplices on $S^1$, let $g:\{0,\ldots,k-1\}\to S$ be injective, and let $F:S\to\mathbb{Z}$. For every $e\in S$, $$\sum_{i}\bigl(\text{if }g(i)=e\text{ then }F(g(i))\text{ else }0\bigr) = \begin{cases} F(e) & \text{if }e\in\mathrm{im}(g),\\ 0 & \text{otherwise.}\end{cases}$$
background
The ambient module lifts the path-level winding/displacement invariant on the circle to singular simplices of $\mathrm{TopCat.sphere},1$, and proves the chain-level identity that winding kills boundaries: the alternating face sum of displacement on any singular $2$-simplex vanishes. That identity, with the once-around generator mapping to $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex here is an element of the singular simplicial set of $S^1$ in degree $1$. Free $1$-chains are integer-valued functions on those simplices (finitely supported). Oriented closed walks are encoded by injective finite families of supported edges; reading off a chain's value at a test edge then reduces to a sum of indicator-selected coefficients.
This lemma is the pure Finset identity that performs that collapse. It does not itself mention winding or homology.
proof idea
Case-split on whether the test edge $e$ lies in the image of $g$.
If yes, obtain a preimage index $i_0$ from membership in the image Finset. Injectivity forces every other index $j$ to satisfy $g(j)\neq e$, so the corresponding if-branches are zero. Finset.sum_eq_single_of_mem therefore reduces the sum to the single term at $i_0$, which equals $F(e)$ after rewriting by $g(i_0)=e$.
If no, every index $i$ has $g(i)\neq e$ (else $e$ would be in the image). Each summand is zero, and Finset.sum_eq_zero finishes.
why it matters
Immediate consumer is edgeCoeff_orientedCyclicChain: the pointwise coefficient of an oriented closed walk equals the sign-unit of the underlying flow on the walk and zero off it. That extraction is exactly this sum identity applied to the walk's injective edge family.
In the module's larger program, free edge-chains of oriented cyclic walks are the concrete cycles against which the winding homomorphism is evaluated. Clean pointwise coefficients keep the comparison map $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$ computable on those generators, supporting the split-injective half of the integer comparison (the generation/surjectivity half still needs a simplicial prism operator Mathlib does not yet supply).
No Recognition forcing-chain landmark (T5–T8, RCL, phi) is touched; this is pure singular-chain bookkeeping inside the circle-winding foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.