edgeSupportCard_sub_lt_of_supported_exact_cancel
plain-language theorem explainer
If a free singular 1-chain p is supported inside c and exactly cancels the coefficient of at least one edge of c, then the support of c − p is strictly smaller than that of c. Anyone proving one-step cyclic extraction or large-support peels on free edge-chains cites this. The proof shows residual support sits inside the original support and drops the cancelled edge, then applies Finset.card_lt_card.
Claim. Let $c,p$ be free singular $1$-chains on $S^1$. If the edge-support of $p$ is contained in the edge-support of $c$, and there exists an edge $e$ in the support of $p$ with $\mathrm{coeff}(p,e)=\mathrm{coeff}(c,e)$, then $\#\mathrm{supp}(c-p)<\#\mathrm{supp}(c)$.
background
The module works with free singular $1$-chains on $\mathrm{TopCat.sphere},1$: finite $\mathbb{Z}$-linear combinations of singular $1$-simplices $f:\Delta^1\to S^1$. The coefficient of an edge $e$ is the Finsupp value $\mathrm{edgeCoeff}(c,e)$, and the edge-support is the finite set of edges with nonzero coefficient; $\mathrm{edgeSupportCard}$ is its cardinality.
The ambient goal of the module is the winding invariant on singular $1$-simplices and the kills-boundaries identity $\mathrm{simplexDisplacement}\circ\partial=0$, which supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Generation (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs cyclic extraction from large-support cycles.
Upstream, $\mathrm{edgeCoeff_sub}$ records that coefficients of a difference are differences of coefficients, and membership in edge-support is equivalent to a nonzero coefficient. Those two facts are the only algebraic inputs here.
proof idea
First prove residual support sits inside original support: if $e$ lies in $\mathrm{supp}(c-p)$ but not in $\mathrm{supp}(c)$, then $\mathrm{coeff}(c,e)=0$, and support-inclusion forces $\mathrm{coeff}(p,e)=0$, so $\mathrm{coeff}(c-p,e)=0$ by $\mathrm{edgeCoeff_sub}$, a contradiction.
From the exact-cancel hypothesis pick $e$ with matching nonzero coefficients. Then $e\in\mathrm{supp}(c)$, but $\mathrm{coeff}(c-p,e)=0$ by $\mathrm{edgeCoeff_sub}$ and $\mathrm{sub_self}$, so $e\notin\mathrm{supp}(c-p)$.
Thus $\mathrm{supp}(c-p)\subsetneq\mathrm{supp}(c)$. Unfold the cardinality definition and apply $\mathrm{Finset.card_lt_card}$.
why it matters
This is the generic support-cardinality bookkeeping for any one-step cyclic extraction proof (doc-comment). Downstream, $\mathrm{edgeSupportCard_sub_orientedCyclic_lt_of_unitCoeff}$ and $\mathrm{edgeSupportCard_sub_scaled_orientedCyclic_lt}$ specialise it to sign-selected oriented closed walks and min-coefficient scaled peels.
Those feed $\mathrm{largeSupportSupportedExactCyclicPeelStep}$ and $\mathrm{largeSupportCyclicEdgeListExtractionStep_of_supportedExactPeel}$, which package a supported exact cyclic peel into the literal large-support extraction target: residual $c-t.\mathrm{chain}$, boundary-zero from the cyclic term, and the strict support drop from this lemma.
In the broader Recognition foundation story this is infrastructure for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (every $1$-cycle homologous to an integer multiple of the fundamental cycle), complementing the already-proved kills-boundaries / split-injective half via $\mathrm{simplexDisplacement}$. It does not itself touch T0–T8 or the RCL; it is pure chain-level bookkeeping on $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.