parallelTwoEdgeFlow_coeff_right
plain-language theorem explainer
For two distinct singular 1-simplices on the circle, the coefficient of the second edge in the signed two-edge parallel flow (first free generator minus second) is exactly -1. Anyone reading off free C₁ coefficients of that obstruction shape cites this. The proof unfolds the flow, subtracts coefficients, and uses freeness plus distinctness to kill the cross term.
Claim. Let $e$ and $f$ be distinct singular $1$-simplices of $S^1$. Writing $\mathrm{free}(e)-\mathrm{free}(f)$ for the corresponding free $C_1$ chain, the coefficient of $f$ in that chain equals $-1$.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$, and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity, with the fundamental loop sending to winding $1$, gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is an element of the singular simplicial set of the circle in degree $1$. The free $C_1$ module is the free abelian group on those simplices; edgeCoeff reads the integer coefficient of a chosen edge. The two-edge parallel flow is the explicit free chain $\mathrm{free}(e)-\mathrm{free}(f)$: one edge with coefficient $+1$ and a second with coefficient $-1$. Upstream lemmas record that free generators have coefficient $1$ on themselves, singles evaluate by a pointwise if-then, and coefficients are linear under subtraction.
proof idea
Unfold the parallel-flow definition to $\mathrm{free}(e)-\mathrm{free}(f)$. Rewrite the target coefficient via linearity of coefficients under subtraction, then apply the self-coefficient lemma so the second summand contributes $1$. It remains to show the coefficient of $f$ in $\mathrm{free}(e)$ is $0$: expand the free generator as a Finsupp single, apply the single-coefficient lemma, and simplify with $e\neq f$. Finish with norm_num on $0-1$.
why it matters
This is the right-hand half of the coefficient bookkeeping for the two-edge parallel-flow obstruction: the companion left-hand statement gives coefficient $+1$ on the first edge. Immediately downstream in the module, those two facts feed the claim that if two distinct singular edges share endpoints, their signed two-edge flow is balanced (in the ledger sense). That balance is the chain-level shape used when comparing parallel edges that realize the same endpoints on $S^1$, tying into the winding-kills-boundaries identity that underwrites the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. No used-by edges are recorded yet; the lemma is local scaffolding for the balanced-flow package rather than a named paper proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.