singleEdgeFlow_zero_boundary_faces_eq
plain-language theorem explainer
A nonzero integer multiple of one singular 1-simplex on S¹ is a cycle only if that simplex is a loop (equal endpoints). Extraction lemmas for balanced free edge-flows cite this when support has size one. The proof is coefficient readout on the free 0-chain: the boundary formula forces n=0 unless the two faces coincide.
Claim. Let $e$ be a singular $1$-simplex of $S^1$ and $n\in\mathbb{Z}$ with $n\neq 0$. If the free singular $1$-chain $n\cdot[e]$ has vanishing boundary under the free singular boundary map, then the terminal $0$-face of $e$ equals its initial $0$-face.
background
The module lifts path winding on $S^1$ to singular simplices and proves that displacement kills boundaries, giving 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 of the topological circle.
Directed faces of such an edge are the two face maps of the simplicial set: the terminal vertex is $\delta_0 e$ and the initial vertex is $\delta_1 e$. Free singular chains are $\mathbb{Z}$-linear combinations of simplices (Finsupp-valued), and the free boundary sends a generator $[e]$ to $[\mathrm{term}]-[\mathrm{init}]$.
A free flow $n\cdot[e]$ is balanced when that boundary vanishes. The present lemma records the elementary incidence obstruction: a nonzero multiple of a single non-loop edge cannot be balanced.
proof idea
Argue by contradiction: assume the two faces differ. Rewrite the zero-boundary hypothesis via linearity and the free-boundary formula on generators to obtain $n\cdot([\mathrm{term}]-[\mathrm{init}])=0$ in the free $0$-chain module.
Evaluate both sides at the terminal vertex (Finsupp coefficient). With distinct endpoints the initial generator contributes $0$ there, so the coefficient is exactly $n$. Hence $n=0$, contradicting the nonzero hypothesis. The only remaining possibility is equal endpoints.
why it matters
This is the residual obstruction in the parallel-edge / singleton-support case of cyclic edge-list extraction on free $1$-cycles of $S^1$. Downstream, singletonSupport_zero_boundary_faces_eq reduces the singleton-support balanced chain to a loop; singleEdgeFlow_decomposesIntoCyclicEdgeLists packages a nonzero single-edge cycle as an already-cyclic decomposition; and supportCard_le_one_extractionStep feeds the one-step extraction required by the finite-flow pipeline.
In the module narrative, winding on $1$-cycles is already a left inverse to the fundamental class. The generation half (every cycle homologous to an integer multiple of the fundamental cycle) needs simplicial prism / subdivision machinery Mathlib does not yet supply; the extraction lemmas here are the combinatorial bookkeeping that isolates loop residuals once support is reduced. No direct T0–T8 forcing step is claimed; the result is pure singular-chain incidence on the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.