largeSupportSupportedExactCyclicPeelStep
plain-language theorem explainer
Defines the stronger large-support peel target on free singular 1-chains of S¹: every nonzero boundary-zero chain with support size greater than one admits a cyclic edge-list term supported inside it that exactly matches the coefficient on at least one shared edge. Homology and extraction arguments cite this Prop as the clean one-step peel hypothesis. The body is a pure Prop package; no proof is attached.
Claim. For every free singular $1$-chain $c$ on $S^1$ with vanishing boundary, $c \neq 0$, and support cardinality strictly greater than $1$, there exists a cyclic singular edge-list term $t$ such that the support of $t$'s chain is contained in the support of $c$, and on at least one edge in that support the integer coefficient of $t$'s chain equals the coefficient of $c$.
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}$. Generation (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a simplicial extraction / subdivision argument that Mathlib singular homology does not yet supply.
Work is in the explicit free $C_1$ module: edgeCoeff reads the $\mathbb{Z}$-coefficient of a singular $1$-simplex, edgeSupport is its finite support, and edgeSupportCard is that support's cardinality. A cyclic singular edge-list term is a closed walk packaged as a free chain. The upstream bookkeeping lemma edgeSupportCard_sub_lt_of_supported_exact_cancel states that if a peel chain $p$ is supported inside $c$ and exactly cancels at least one supported edge, then $\mathrm{card}(\mathrm{supp}(c-p)) < \mathrm{card}(\mathrm{supp}(c))$.
proof idea
No proof: this is a bare Prop definition. It packages four hypotheses on a free $1$-chain $c$ (boundary zero via the free singular boundary map, nonzero, support card $>1$) and asserts existence of a cyclic edge-list term whose chain sits inside $\mathrm{supp}(c)$ and matches $c$ on at least one coefficient. Downstream proofs discharge the literal large-support extraction step by feeding this Prop into the generic support-drop lemma.
why it matters
This is the cleaner intermediate target for large-support cyclic extraction on free $1$-chains of $S^1$. The sole downstream consumer is largeSupportCyclicEdgeListExtractionStep_of_supportedExactPeel, which (quoting its doc) "packages the residual as $c - t.\mathrm{chain}$, gets boundary-zero from the cyclic term, and gets the strict support drop from edgeSupportCard_sub_lt_of_supported_exact_cancel."
In the module's program, that extraction step is part of the generation half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$: peeling cyclic edge-lists down to a multiple of the fundamental loop. The winding/kills-boundaries identity already gives the left-inverse half; this Prop isolates the one-step peel needed for the converse. It does not itself touch the forcing chain (T0–T8) or RCL, but sits in the foundational circle-homology layer those landmarks rely on for discrete period and winding bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.