edgeSupportCard
plain-language theorem explainer
Support size of a free singular 1-chain on the circle: how many distinct edges carry a nonzero integer coefficient. Extraction and generation arguments cite it as the discrete measure that must strictly decrease under each cyclic peel. The body is the Finset cardinality of the Finsupp support.
Claim. For a free singular $1$-chain $c$ on $S^1$ (an element of the free $\mathbb{Z}$-module on singular $1$-simplices), the edge-support cardinality is the number of singular $1$-simplices with nonzero coefficient in $c$.
background
The module lifts path-level winding on the circle to singular simplices of $S^1$ and proves that displacement kills boundaries, giving the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Free singular $1$-chains are elements of the free $\mathbb{Z}$-module on actual singular $1$-simplices; each chain is a finitely supported integer combination of edges.
Support means the finite set of simplices with nonzero coefficient (the Finsupp support). Edge-support cardinality is that set's size. Downstream extraction work treats nonzero balanced free edge-flows by peeling cyclic edge-list pieces and needs a nonnegative integer that drops at each successful peel; this definition supplies that integer.
proof idea
One-line definition: return the Finset cardinality of the underlying Finsupp support of the free chain. No lemmas or tactics.
why it matters
Bookkeeping primitive for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module already has winding as a left inverse to the fundamental class (injective half via covering-space winding); surjectivity needs every free $1$-cycle homologous to an integer multiple of the fundamental cycle, approached by decomposing balanced free edge-flows into cyclic edge lists.
Parents include the one-step extraction target (every nonzero balanced free edge-flow splits into a cyclic piece plus a residual of strictly smaller support), the large-support handoff, the zero-support characterization, and the strict-decrease lemmas for supported exact cancel, unit-coefficient oriented cyclic peels, and min-coefficient scaled peels. Without a well-defined support size, the support-decreasing induction cannot start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.