orientedEdgeOfCoeff
plain-language theorem explainer
Packages a singular 1-simplex with the traversal orientation fixed by the sign of its coefficient in a free 1-chain on S¹. Positive coefficients run forward; non-positive run backward. Downstream cycle-extraction and next-edge lemmas cite it as the canonical oriented reading of a supported edge. The body is a two-field structure constructor.
Claim. Given a free singular $1$-chain $c$ on $S^1$ and a singular $1$-simplex $e$, form the oriented edge whose underlying simplex is $e$ and whose orientation is forward if the coefficient of $e$ in $c$ is positive, and backward otherwise.
background
The module works at the level of singular simplices of $\mathrm{TopCat.sphere},1$, lifting the path winding/displacement invariant of CircleWinding so that it becomes a homology invariant. Free $1$-chains live in the free $\mathbb{Z}$-module on singular $1$-simplices; the coefficient of an edge $e$ in such a chain $c$ is the evaluation of the underlying function at $e$.
An oriented singular edge is a pair (simplex, orientation), where orientation is either forward or backward and determines which endpoint is initial versus terminal. The helper that chooses orientation from an integer sends positive coefficients to forward and all others to backward. This definition simply glues those two pieces: keep the given simplex and orient it by the sign of its coefficient in the ambient flow.
proof idea
Definitional constructor, not a proof. The edge field is the input simplex $e$. The orientation field is orientationOfCoeff applied to edgeCoeff c e, i.e. the integer coefficient of $e$ in the free chain $c$. No lemmas are invoked.
why it matters
This is the standard way the module reads a supported edge of a free edge-flow in the direction the flow itself suggests. Local positivity at the oriented terminal, existence of a compensating negative contribution in a balanced flow, and the successor-edge theorem all quantify over this oriented package. Higher up it feeds oriented closed-walk extraction for nonzero balanced flows and the one-step directed-cycle extraction that splits such a flow into a directed-cycle piece plus a strictly smaller $\ell^1$ residual.
In the module's larger program, those extractions support the chain-level winding story that, together with the kills-boundaries identity for $2$-simplices, gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The definition itself is pure bookkeeping; the mathematical content sits in the lemmas that use the oriented reading.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.