boundaryIncidenceSum_add
plain-language theorem explainer
The incidence sum that extracts a vertex boundary coefficient from a free singular 1-chain on S¹ is additive in the chain. Anyone equating boundary coefficients to finite support incidence sums cites this. Proof unfolds the sum definition and applies Finsupp add-index with ring cleanup on the incidence coefficients.
Claim. Let $f,g$ be free singular $1$-chains on $S^1$ and let $v$ be a singular $0$-simplex. Then the incidence sum of $f+g$ at $v$ equals the sum of the incidence sums of $f$ and of $g$ at $v$: $\mathrm{Inc}(f+g,v)=\mathrm{Inc}(f,v)+\mathrm{Inc}(g,v)$.
background
This module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves that simplex displacement kills boundaries, the chain-level fact needed for a winding homomorphism on $1$-cycles that left-inverts the fundamental class (half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$).
A singular $0$-simplex is a point of the singular simplicial set of $S^1$. Free singular $1$-chains are the free $\mathbb{Z}$-module on singular $1$-simplices. The incidence sum at a vertex $v$ is $\sum_e n_e\cdot\mathrm{inc}(e,v)$ over the finitely supported edge coefficients of a chain $c$; the upstream definition states it is "the incidence-sum expression for the boundary coefficient of a finite free edge-chain," the local finite-support algebra for the support-decreasing graph argument.
proof idea
Unfold the definition of the incidence sum (a Finsupp.sum of coefficient times incidence). Rewrite by Finsupp.sum_add_index', which splits the sum over $f+g$ into the sum of the two sums once the summand is shown additive in the coefficient and zero at zero. Both side conditions are pure integer arithmetic on $n\mapsto n\cdot\mathrm{inc}(e,v)$: ring_nf for the zero-coefficient case and ring for bilinearity in the two coefficients.
why it matters
Feeds vertexBoundaryCoeff_eq_incidenceSum_holds, which asserts that the true boundary coefficient of any finite free edge-flow equals this incidence sum over its support. That equality is the finite-support algebra step in the support-decreasing graph proof that boundary coefficients are well-defined and computable from incidence data.
In the module's larger program, incidence bookkeeping sits under the kills-boundaries identity for simplex displacement and the winding homomorphism that realises the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation (surjectivity) half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No RS forcing-chain landmark (T5–T8, RCL) is directly invoked here; the result is pure singular-chain algebra on the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.