singletonSupport_zero_boundary_faces_eq
plain-language theorem explainer
A free singular 1-chain on S¹ that is a cycle and has singleton support must be supported on a loop edge (initial vertex equals terminal). Anyone reducing residual balanced edge-flows in the parallel-edge obstruction case cites this. The proof rewrites the chain as a scalar multiple of that single free generator, then applies the single-edge zero-boundary face identity.
Claim. Let $c$ be a free singular $1$-chain on $S^1$ and $e$ a singular $1$-simplex. If the support of $c$ is exactly $\{e\}$ and $\partial_1 c = 0$, then the terminal vertex of $e$ equals its initial vertex (so $e$ is a loop).
background
This module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves that simplex displacement kills boundaries, giving 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 $S^1$ in degree $1$. Free $1$-chains are finitely supported integer combinations of those edges. The edge support is the finite set of simplices with nonzero coefficient; the edge coefficient is the integer at a given edge. Initial and terminal vertices are the two face maps $\delta_1$ and $\delta_0$ of the edge (matching the signed boundary terms).
The hypothesis $\partial_1 c=0$ means $c$ is a $1$-cycle in the free singular chain complex. The companion fact for a pure multiple of one free generator already forces that generator to be a loop when the boundary vanishes; the present statement extends that to any chain whose support is a singleton.
proof idea
From singleton support, $e$ lies in the support, so its coefficient is nonzero. Apply eq_zsmul_freeMk_of_edgeSupport_eq_single to rewrite $c$ as that coefficient times the free generator on $e$. Substitute into the zero-boundary hypothesis and finish by singleEdgeFlow_zero_boundary_faces_eq, which already concludes initial equals terminal for a nonzero multiple of a single edge with vanishing boundary.
why it matters
Doc-comment places this as the residual obstruction in the parallel-edge case: a one-edge balanced residual cannot sit on a non-loop edge. It closes the singleton-support branch when analyzing free $1$-cycles whose boundary vanishes, feeding the chain-level winding story that, with simplexDisplacement_boundary and the fundamental-loop normalization, yields the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
No downstream uses are recorded yet; the lemma is local infrastructure inside CircleWindingChain for residual flow bookkeeping. It does not touch the forcing chain T0–T8 or RCL directly; it is pure singular-homology support for the circle winding invariant that Recognition uses when comparing discrete recognition cycles to continuous $S^1$ homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.