edgeSupportCard_sub_scaled_orientedCyclic_lt
plain-language theorem explainer
Given a free singular 1-chain and an injective family of k support edges, some positive integer scale of the sign-selected oriented closed walk through that family strictly shrinks edge-support cardinality. Homology and cycle-extraction arguments cite it as the exact cyclic peel step. The proof picks the walk edge of minimal absolute coefficient and feeds an exact-cancel support lemma.
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 $k>0$ and every $g(i)$ in the edge support of $c$. Then there exists an integer $m>0$ such that the edge-support cardinality of $c-m\cdot P$ is strictly smaller than that of $c$, where $P$ is the oriented cyclic chain on the image of $g$ (coefficients $\pm 1$ matching the sign of $c$ on the walk, zero off it).
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Chains are handled in an explicit free $C_1$ module: edgeCoeff reads the integer coefficient of a singular $1$-simplex, and edge support is the finite set where that coefficient is nonzero.
An oriented cyclic chain on an injective family $g$ is the closed walk with coefficients $\pm 1$ equal to the sign of the underlying flow on the image of $g$ and zero elsewhere (pointwise formula in edgeCoeff_orientedCyclicChain). Scaling by $m\in\mathbb{Z}$ multiplies coefficients by $m$. The present lemma is pure support bookkeeping for peeling such walks off a chain without enlarging support.
Upstream, membership in edge support is equivalent to a nonzero coefficient, and the oriented-chain support is exactly the image of $g$ when $g$ is injective.
proof idea
Define absolute coefficients on the $k$ walk edges and pick an index $i_0$ minimizing that absolute value; set $m$ to that minimum. Nonzero support membership forces $m>0$.
Apply edgeSupportCard_sub_lt_of_supported_exact_cancel with two obligations. First, every edge in the support of $m\cdot P$ already lies in the support of $c$: a nonzero scaled coefficient implies a nonzero coefficient of $P$, hence (by the oriented-chain support identity under injectivity) the edge is some $g(i)$, which sits in the support of $c$ by hypothesis.
Second, exact cancel at $g(i_0)$: edgeCoeff_zsmul and edgeCoeff_orientedCyclicChain give that the scaled coefficient equals $m$ times the sign unit of the original coefficient, and intNatAbs_mul_signUnit_eq_self identifies that with the original coefficient itself. Thus the min-coefficient edge cancels exactly and support cardinality drops.
why it matters
This is the support-cardinality engine for a true exact cyclic peel on free singular $1$-chains: scale the sign-selected oriented closed walk by the minimal absolute coefficient so one edge cancels exactly and no new edges appear. Downstream, largeSupportOrientedScaledExtractionStep_holds invokes it after producing an oriented cyclic family from a balanced nonzero chain, discharging the large-support oriented extraction step unconditionally (only nonzero balanced flow is essential).
In the module's program, winding/displacement on singular simplices plus the kills-boundaries identity give injectivity of the comparison $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. Generation (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs subdivision/prism technology Mathlib singular homology still lacks; cyclic extraction lemmas like this are the combinatorial half of that generation story. No direct appeal to T0–T8 or the RCL is required here; the result is pure chain-level support arithmetic inside the $S^1$ homology package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.