edgeSupportCard_sub_orientedCyclic_lt_of_unitCoeff
plain-language theorem explainer
If an injective family of edges forms a sign-selected oriented closed walk inside the support of a free singular 1-chain and at least one of those edges has coefficient ±1, subtracting the walk strictly decreases support cardinality. Anyone proving one-step cyclic extraction or large-support peeling on free C₁ chains cites this. The proof is a short term application of the generic supported exact-cancel cardinality lemma, feeding the walk's support and unit-coefficient identities.
Claim. Let $c$ be a free singular $1$-chain on $S^1$, and let $g:\mathrm{Fin}\,k\to\{\text{singular $1$-simplices}\}$ be injective with every $g(i)$ in the edge-support of $c$. If some coefficient of $c$ on the image of $g$ has absolute value $1$, then $\mathrm{card}(\mathrm{supp}(c-p))<\mathrm{card}(\mathrm{supp}(c))$, where $p$ is the sign-selected oriented closed walk along $g$ (coefficient $+1$ or $-1$ according to the sign of $c$ on each edge of the walk, and $0$ off the walk).
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Parallel to that invariant work, free $C_1$ chains are handled explicitly: edgeCoeff is the integer coefficient of a singular $1$-simplex, edgeSupport is its finite support, and edgeSupportCard is the cardinality of that support.
An oriented closed walk along an injective edge family $g$ is the free chain whose coefficient on each image edge is the sign-unit of the ambient flow $c$ (namely $+1$ if $c$ is positive there, else $-1$) and zero off the image. Upstream, the support of that walk equals the image of $g$, and its pointwise coefficients are exactly those sign-units on the image.
The generic bookkeeping lemma states that if a peel chain $p$ is supported inside $c$ and exactly cancels at least one supported edge of $c$, then $\mathrm{card}(\mathrm{supp}(c-p))<\mathrm{card}(\mathrm{supp}(c))$. The present result specialises that lemma to unit-coefficient oriented cyclic peels.
proof idea
One-shot application of the generic lemma edgeSupportCard_sub_lt_of_supported_exact_cancel with peel $p=$ the oriented cyclic walk along $g$.
Support inclusion: rewrite the walk support via edgeSupport_orientedCyclicChain (equals the image of $g$) and use that every $g(i)$ already lies in $\mathrm{supp}(c)$.
Exact cancel: pick the index $i$ with $\lvert c(g(i))\rvert=1$. The walk support membership of $g(i)$ is immediate from the image characterisation. On that edge, edgeCoeff_orientedCyclicChain reduces the walk coefficient to the sign-unit of $c(g(i))$, and eq_sign_unit_of_natAbs_eq_one upgrades $\mathrm{natAbs}=1$ to equality with that sign-unit, so the walk coefficient equals the ambient coefficient.
why it matters
Support-cardinality descent is the engine of cyclic extraction: each successful peel removes at least one edge and introduces none outside the original support, so induction on support size terminates. The doc-comment isolates exactly this cardinality half of large-support extraction, separating it from the harder encoding of mixed-orientation walks in older one-scalar cyclic-edge-list formats.
In the broader CircleWindingChain programme, such peels feed generation arguments toward the surjective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (every $1$-cycle homologous to an integer multiple of the fundamental cycle). The module already has the kills-boundaries identity and the winding left-inverse on the fundamental loop; support-reducing cyclic peels are the combinatorial counterpart needed when Mathlib still lacks a full simplicial prism or subdivision operator for the generation direction.
No downstream consumers are wired yet in the graph (used_by empty), so this is infrastructure waiting on the true exact cyclic peel and large-support extraction theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.