parallelTwoEdgeFlow_ne_zero
plain-language theorem explainer
Distinct singular 1-simplices on the circle yield a nonzero free 1-chain with coefficients +1 and −1 (the parallel two-edge flow). Anyone classifying support branches in the singular H₁(S¹) computation cites this nonvanishing. The argument is a short contradiction: the left edge would have coefficient 0 if the chain vanished, but that coefficient is forced to 1.
Claim. Let $e$ and $f$ be singular $1$-simplices of $S^1$. If $e \neq f$, then the free integer $1$-chain $e - f$ is nonzero in the free module on singular $1$-simplices.
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 of singular $2$-simplices. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
A singular $1$-simplex is an element of the singular simplicial set of $S^1$ in degree $1$. The free module on those simplices is the explicit $C_1$ used here; edgeCoeff reads the integer coefficient of a chosen edge. The parallel two-edge flow is the elementary chain $e-f$ (one edge with coefficient $+1$, another with $-1$), the obstruction shape for two-edge parallel support.
Upstream, the left-edge coefficient lemma already records that when $e\neq f$, the coefficient of $e$ in this flow equals $1$.
proof idea
Term-mode contradiction. Assume the parallel two-edge flow vanishes. Rewrite the left-edge coefficient identity under that hypothesis: the coefficient of $e$ in the zero chain equals $1$. The zero chain has all coefficients $0$, so one obtains $0=1$ in $\mathbb{Z}$, which norm_num rejects. The only nontrivial input is the left-edge coefficient lemma for distinct edges.
why it matters
Nonvanishing of $e-f$ for $e\neq f$ is the elementary freeness fact that puts a distinct two-edge parallel flow into the large-support branch of the circle $H_1$ bookkeeping (the next declaration in the file). Without it, support-case splits on free $1$-chains would be ill-founded.
In the broader module story this sits under the winding homomorphism that left-inverts the fundamental class of $S^1$, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. No downstream consumers are wired yet; the lemma is local infrastructure for the free-chain case analysis rather than a forcing-chain (T0–T8) landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.