exists_negative_edgeContribution_at_oriented_terminal
plain-language theorem explainer
In a free 1-chain with vanishing boundary, any supported non-loop edge that contributes positively at its oriented terminal forces some other supported edge to contribute negatively at that same vertex. Cycle-chasing and successor-edge arguments on singular 1-chains of S¹ cite this. The proof reduces the boundary-zero hypothesis to a finite integer sum that is zero yet has a strictly positive term, then invokes a generic sum lemma.
Claim. Let $c$ be a finitely supported free singular $1$-chain on $S^1$ with $\partial c = 0$. Let $e$ be an edge in the support of $c$ whose sign-selected orientation is not a loop, and write $v$ for its terminal vertex. Then there exists a supported edge $e'$ such that the contribution of $e'$ to the boundary coefficient of $c$ at $v$ is strictly negative.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, the chain-level fact behind the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Here the focus is the free singular $1$-chain algebra used to walk along cycles.
A free $1$-chain $c$ has finite edge support. At each singular $0$-simplex $v$, the boundary incidence sum is $\sum_e n_e\cdot\mathrm{inc}(e,v)$, equivalently the finite sum of per-edge contributions over the support. The hypothesis $\partial c=0$ forces every such incidence sum to vanish: boundaryIncidenceSum_eq_zero_of_boundary_zero'.
For a supported non-loop edge, the sign-selected orientation has a well-defined initial and terminal vertex. At that terminal, the contribution of the edge itself is strictly positive (edgeContribution_pos_at_oriented_terminal). The present lemma turns that local positivity plus global balance into existence of a compensating negative contribution.
proof idea
Set $v$ to the oriented terminal of $e$. From $\partial c=0$, the incidence sum at $v$ is zero. Rewrite that sum as the explicit finite sum of edge contributions over the support. The contribution of $e$ at $v$ is strictly positive by the oriented-terminal positivity lemma (using that $e$ is supported and not a loop). Apply the generic fact that a finite integer sum equal to zero with one strictly positive summand must have some strictly negative summand, yielding the required $e'$.
why it matters
This is the algebraic core of the local successor-edge step. Downstream, exists_next_orientedEdge_from_terminal quotes it to produce a supported edge whose sign-selected orientation starts at the terminal of a given non-loop oriented edge in a balanced flow. That successor relation is how one walks a closed singular $1$-cycle edge by edge.
In the module's larger program, such walks feed the comparison of free $1$-cycles with integer multiples of the fundamental loop, the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The kills-boundaries identity for simplex displacement already gives the winding homomorphism as a left inverse to the fundamental class; successor-edge existence is infrastructure for the converse direction once prism/subdivision tools are available. No Recognition forcing-chain landmark (T5–T8, RCL) is invoked here: the result is pure singular-chain bookkeeping on $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.