parallelTwoEdgeFlow_boundary_zero
plain-language theorem explainer
Two singular edges on S¹ that share both endpoints form a 1-cycle: the free-module boundary of their signed difference vanishes. Anyone building explicit cycle generators or parallel-flow obstructions in the singular chain complex of the circle will cite this. The proof expands the free boundary on each edge, substitutes the shared endpoints, and cancels by abelian arithmetic.
Claim. Let $e,f$ be singular $1$-simplices on $S^1$. If the terminal vertex of $e$ equals that of $f$ and the initial vertex of $e$ equals that of $f$, then the free singular boundary of the chain $e-f$ is the zero $0$-chain.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that displacement kills boundaries, the chain-level fact needed for a homology invariant. The long-term goal is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is a continuous map $\Delta^1\to S^1$ in the singular simplicial set. Its initial and terminal vertices are the two face maps $\delta_1$ and $\delta_0$. The free boundary sends each directed edge to $\mathrm{freeMk}(\mathrm{terminal})-\mathrm{freeMk}(\mathrm{initial})$. The parallel two-edge flow is the free $1$-chain $\mathrm{freeMk}(e)-\mathrm{freeMk}(f)$: coefficient $+1$ on one edge and $-1$ on the other.
proof idea
Unfold the parallel flow to $\mathrm{freeMk}(e)-\mathrm{freeMk}(f)$. Apply linearity of the free boundary and the evaluation lemma that sends each free generator to terminal-minus-initial. The resulting $0$-chain is
$(\mathrm{term}(e)-\mathrm{init}(e))-(\mathrm{term}(f)-\mathrm{init}(f))$.
Rewrite with the two endpoint hypotheses, then finish by abel (the two differences cancel).
why it matters
In the CircleWindingChain development this is the elementary cycle check for the two-edge parallel-flow shape: same endpoints imply the signed difference is a genuine $1$-cycle. That shape is the natural obstruction when two distinct edges connect the same pair of vertices, and balanced boundary is the first filter before winding or support arguments.
The module's main theorem is the kills-boundaries identity for simplex displacement (the $2$-simplex telescoping that makes winding a homology invariant). This lemma sits one level down: it certifies that parallel flows are cycles so they can later be compared by winding. No downstream consumers are wired yet (used_by is empty), and the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ still needs a simplicial prism/subdivision operator Mathlib does not supply. No T0–T8 forcing step is touched directly; the link is foundational topology for the circle's winding homomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.