edgeSupport_orientedCyclicChain
plain-language theorem explainer
The free 1-chain of a sign-oriented closed walk on an injective edge family has support exactly the image of that family. Cycle-peel and ℓ¹ bookkeeping cite it to identify which edges carry the walk. The proof is a pointwise case split: coefficients are the nonzero sign-units on the image and zero off it.
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. The support of the oriented closed-walk chain built from $c$ along $g$ equals the finite image of $g$.
background
This module lifts path 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}$. Free $1$-chains are integer finitely supported functions on singular $1$-simplices of $\mathrm{TopCat.sphere},1$; edgeSupport is that Finsupp support, equivalently the set of edges with nonzero coefficient.
An oriented closed walk through an injective family $g$ is the free chain summing, at each $g(i)$, the generator with coefficient equal to the sign-unit of $c$ at that edge ($+1$ if the ambient coefficient is positive, $-1$ otherwise). Upstream, the pointwise formula states that this coefficient is that sign-unit on the image of $g$ and $0$ off it; the sign-unit is never zero.
proof idea
Extensionality on edges. Rewrite membership in support as nonzero coefficient, then substitute the pointwise coefficient of the oriented walk. Case on whether $e$ lies in the image of $g$: on the image the coefficient is a sign-unit, hence nonzero by sign_unit_ne_zero; off the image it is $0$. Both directions of the desired equality follow.
why it matters
Identifies the walk's support with the edge family image, so cardinality and $\ell^1$ size equal $k$. Downstream: chainL1_orientedCyclicChain gets $\ell^1=k$ in one rewrite; chainL1_sub_orientedCyclic uses it for the exact $\ell^1$ drop of one directed-cycle peel; edgeSupportCard_sub_orientedCyclic_lt_of_unitCoeff and the scaled variant use it for strict support shrinkage when peeling unit or min-coefficient walks.
These peels are the support-cardinality half of extracting large cyclic support from balanced flows on $S^1$, feeding the generation/surjectivity side of the integer comparison map for $H_1(S^1;\mathbb{Z})$ that the module doc flags as still needing a simplicial prism or subdivision operator. No T0–T8 forcing step is touched directly; the landmark is the homology-invariant winding package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.