parallelTwoEdgeFlow_largeSupport
plain-language theorem explainer
When two distinct singular 1-simplices on the circle form a parallel flow (coefficients +1 and -1), the free edge-chain has support cardinality strictly larger than one. Anyone case-splitting finite free flows by support size for cyclic edge-list extraction cites this. The proof rewrites through the exact support-cardinality-two lemma and finishes by arithmetic.
Claim. Let $e$ and $f$ be distinct singular $1$-simplices on $S^1$. Then the free $1$-chain $e-f$ has edge-support cardinality strictly greater than $1$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves the chain-level identity that makes it a homology invariant: simplex displacement kills boundaries. Together with the fact that the once-around generator has winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular one-simplex is a continuous map $\Delta^1\to S^1$ in the singular simplicial set. Free edge-chains are finitely supported integer combinations of such simplices; the edge-support cardinality of a chain is the number of simplices with nonzero coefficient.
The parallel two-edge flow is the obstruction shape with coefficient $+1$ on one singular edge and $-1$ on another. Upstream, whenever the two edges are distinct, that free chain has support cardinality exactly two.
proof idea
Term-mode one-liner. Rewrite the goal by the upstream support-cardinality lemma for a distinct parallel two-edge flow, which replaces the left-hand side by $2$. Then norm_num closes $1<2$.
why it matters
Places the distinct two-edge parallel flow in the large-support branch of the finite-flow extraction taxonomy. The file immediately contrasts this with the support-cardinality-one subcase: a nonzero single-edge free flow with zero boundary is already a cyclic edge-list decomposition. That case split is part of extracting cyclic edge lists from free $1$-chains with vanishing boundary, which feeds the generation (surjectivity) half of the integer comparison map for $H_1(S^1)$. The module already has the kills-boundaries identity and the winding left-inverse to the fundamental class; full generation still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No recorded downstream users yet; the lemma is local infrastructure for the large-support arm.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.