parallelTwoEdgeFlow_supportCard
plain-language theorem explainer
A free 1-chain that places coefficient +1 on one singular edge of S¹ and −1 on a distinct second edge has support of size exactly two. Anyone classifying parallel-flow obstruction shapes by support size cites this. The proof rewrites the support to the two-point set and simplifies the cardinality.
Claim. Let $e$ and $f$ be distinct singular $1$-simplices on $S^1$. The free singular $1$-chain with coefficient $+1$ on $e$ and $-1$ on $f$ has support cardinality $2$.
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 edge-chains are finitely supported $\mathbb{Z}$-linear combinations of such simplices; edgeSupport is the underlying finite set of simplices with nonzero coefficient, and edgeSupportCard is its cardinality.
The parallel two-edge flow is the obstruction shape $\mathrm{freeMk}(e)-\mathrm{freeMk}(f)$: coefficient $+1$ on one edge and $-1$ on another. Upstream, when $e\neq f$, the support identity already identifies that support with the two-point set ${e,f}$.
proof idea
Unfold the cardinality definition to (edgeSupport (parallelTwoEdgeFlow e f)).card = 2. Rewrite the support via the upstream support theorem for distinct edges, obtaining {e, f}. Then simp with the distinctness hypothesis finishes the two-element cardinality.
why it matters
Feeds the immediate parent parallelTwoEdgeFlow_largeSupport, which places a distinct two-edge parallel flow in the large-support branch ($1 < \mathrm{card}$). That branch is part of the chain-level bookkeeping around free edge-chains used while building the winding homomorphism on $1$-cycles.
In the module's program, winding on singular $1$-simplices plus the kills-boundaries identity supply the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Support-size facts keep parallel-flow shapes out of the zero and single-edge cases, so they cannot masquerade as trivial or fundamental-cycle generators. No T0–T8 forcing step is settled here; this is pure singular-chain infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.