initial_eq_of_negative_edgeContribution
plain-language theorem explainer
If a singular 1-edge contributes negatively to the boundary coefficient at a vertex v, the sign-selected orientation of that edge has initial vertex v. Flow and cycle-support arguments on free singular 1-chains of S¹ cite this local incidence fact. The proof is pure case analysis on the sign of the edge coefficient and endpoint equalities, closed by omega.
Claim. Let $c$ be a free singular $1$-chain on $S^1$, $e$ a singular $1$-simplex, and $v$ a singular $0$-simplex. If the contribution of $e$ to the boundary coefficient of $c$ at $v$ is strictly negative, then the initial vertex of the sign-selected orientation of $e$ (forward when the coefficient of $e$ is positive, reversed when negative) equals $v$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Chains are handled in an explicit free $C_1$ module on singular $1$-simplices of $\mathrm{TopCat.sphere},1$.
For a directed singular edge $e$, the terminal vertex is the $0$-face and the initial vertex the $1$-face. The incidence coefficient at $v$ is $+1$ at the terminal, $-1$ at the initial, and their algebraic sum if both coincide. Edge contribution is the product of the integer coefficient of $e$ in $c$ with that incidence number.
The sign-selected oriented edge reads $e$ forward when its coefficient is positive and reversed when negative, so its initial vertex is the endpoint that receives the negative incidence contribution after the sign is absorbed.
proof idea
Unfold contribution as coefficient times incidence, and unfold the oriented edge's initial vertex via the orientation-of-coefficient map. Case on whether the raw edge coefficient is positive.
If positive, the oriented initial is the geometric initial. Subcases on whether $v$ equals initial or terminal: equality of initial gives the goal; terminal-only or neither forces the contribution nonnegative, contradicting hneg via simp and omega.
If not positive, either the coefficient is zero (contribution zero, contradiction) or strictly negative. Then the oriented initial is the geometric terminal; matching $v$ to terminal wins, while initial-only or neither again makes the contribution nonnegative and omega closes.
why it matters
This is a local incidence lemma for oriented support of free $1$-chains. It feeds directly into exists_next_orientedEdge_from_terminal, the local successor-edge theorem: in a balanced flow (boundary zero), a supported non-loop oriented edge has a supported edge whose sign-selected orientation starts at its terminal vertex.
That successor step is part of walking supported cycles on $S^1$ in the CircleWindingChain development, which builds the chain-level winding invariant and the injective comparison $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$. The module doc stresses that generation (surjectivity) remains open pending a simplicial prism or subdivision operator Mathlib does not yet supply; this lemma is on the proved injective/support side only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.