edgeContribution_pos_at_oriented_terminal
plain-language theorem explainer
A supported non-loop edge in a free singular 1-chain, read in the orientation selected by the sign of its coefficient, contributes a strictly positive integer to the boundary coefficient at its oriented terminal vertex. Homology and flow arguments on S¹ cite this as the local positivity step that forces a compensating outgoing edge at a balanced vertex. The proof is a two-case sign split on the edge coefficient, followed by simplification of the incidence formula.
Claim. Let $c$ be a free singular $1$-chain on $S^1$ and let $e$ be a singular $1$-simplex in the support of $c$. Write $e^\pm$ for $e$ reoriented by the sign of its coefficient in $c$, and assume the initial and terminal vertices of $e^\pm$ are distinct. Then the contribution of $e$ to the boundary coefficient of $c$ at the terminal vertex of $e^\pm$ is strictly positive.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that simplex displacement kills boundaries: the alternating face sum of displacement on any singular $2$-simplex vanishes. That identity, with the once-around generator mapping to $1$, yields the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The free $C_1$ module is handled explicitly. The coefficient of an edge $e$ in a chain $c$ is the integer value of $c$ at $e$; the support is the finite set where that coefficient is nonzero. Terminal and initial vertices of a directed singular edge are the face maps $\delta_0$ and $\delta_1$. The incidence coefficient at a vertex $v$ is $+1$ at the terminal, $-1$ at the initial, and their algebraic sum if the endpoints coincide.
Edge contribution is the product of the raw edge coefficient with the incidence coefficient at a chosen vertex. Orientation by coefficient sign flips the raw edge when the coefficient is negative, so the oriented terminal is the geometric end of the positively counted arrow.
proof idea
Support membership immediately gives a nonzero edge coefficient. Split on the sign of that coefficient.
If the coefficient is positive, the sign-selected orientation is the raw edge, so the non-loop hypothesis says initial $\neq$ terminal. Unfolding edge contribution and incidence at the oriented terminal yields coefficient times $+1$, which is positive.
If the coefficient is not positive, it is strictly negative. The oriented edge is the reverse of the raw edge, so the oriented terminal is the raw initial vertex; the non-loop hypothesis becomes terminal $\neq$ initial on the raw edge. Unfolding again gives a negative coefficient times the incidence $-1$ at the raw initial, hence a positive product (finished by omega).
why it matters
Local positivity at the oriented terminal is the algebraic engine behind next-edge existence in balanced singular $1$-chains. The sole downstream consumer is exists_negative_edgeContribution_at_oriented_terminal: in a chain with vanishing free boundary, a positive contribution at a vertex forces some negative contribution at the same vertex; applied to a sign-selected supported edge, that is the core of the next-edge step.
In the broader CircleWindingChain program this feeds the constructive reading of $1$-cycles on $S^1$ as balanced flows, which pairs with the winding homomorphism (left inverse to the fundamental class) toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module already has the kills-boundaries identity and the generator evaluation; the remaining generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. This lemma is pure chain algebra and does not itself touch the Recognition forcing chain (T0–T8), but it sits in the foundation layer that underwrites topological invariants used elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.