orientedCyclicChain
plain-language theorem explainer
Packages an injective family of singular 1-simplices into the free integer 1-chain that is the sum of those edges, each oriented by the sign of its coefficient in an ambient free flow. Cycle-extraction and ℓ¹-peeling arguments cite it as the directed closed-walk piece peeled from a balanced flow. The body is a finite sum of the oriented-edge chains of the family.
Claim. Given a free singular $1$-chain $c$ on $S^1$ and a family $g:\mathrm{Fin}\,k\to\{\text{singular }1\text{-simplices of }S^1\}$, form the free $1$-chain $\sum_{i=0}^{k-1} e_i^{\mathrm{or}}$, where each $e_i^{\mathrm{or}}$ is the edge $g(i)$ oriented by the sign of its coefficient in $c$.
background
The module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular one-simplex is an element of the singular simplicial set of $S^1$ in degree $1$. Free singular one-chains are the free $\mathbb{Z}$-module on those simplices. For a flow $c$ and an edge $e$, the oriented edge of coefficient takes $e$ with orientation equal to the sign of the coefficient of $e$ in $c$, so the associated chain is $\pm e$ according as that coefficient is positive or negative.
The present definition assembles a finite injective family of such edges into one free chain: the candidate directed closed walk used throughout the cycle-extraction bookkeeping.
proof idea
Definitional one-liner: unfold as the finite sum over $i:\mathrm{Fin},k$ of the free chain carried by the oriented edge of coefficient of $c$ at $g(i)$. No lemmas are applied; noncomputability is inherited from the free-module and orientation infrastructure.
why it matters
This is the atomic directed-cycle piece in the free-edge-flow calculus on $S^1$. Downstream, the pointwise coefficient theorem records that on the walk the coefficient is the sign-unit of the ambient flow and off the walk it is zero; the $\ell^1$ identity shows the walk has size exactly $k$; subtracting it from a balanced flow lowers $\ell^1$ by exactly $k$.
Those facts feed directed-cycle extraction: every nonzero balanced free edge-flow splits as one directed-cycle term plus a balanced residual of strictly smaller $\ell^1$. Support-cardinality variants (unit-coefficient peel, min-coefficient scaled peel) also subtract this chain or a positive multiple of it.
In the broader Recognition setting the construction supports the generation half of the integer comparison map on $H_1(S^1)$, complementing the winding-kills-boundaries identity already proved in the module. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure singular-chain scaffolding for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.