orientedCoeff_pos_of_mem_edgeSupport
plain-language theorem explainer
Any edge in the support of a free singular 1-chain has strictly positive coefficient once read in the orientation selected by the sign of its raw coefficient. Algebraic topologists working the circle winding / H₁(S¹) comparison use this to treat support edges as positively weighted directed edges. The proof is a two-case split on the sign of the raw coefficient, using support-membership as nonzero and integer arithmetic.
Claim. Let $c$ be an element of the free $\mathbb{Z}$-module on singular $1$-simplices of $S^1$, and let $e$ be a singular $1$-simplex in the support of $c$. Then the oriented coefficient of $e$ in $c$ (the raw coefficient if positive, its negation if negative) is strictly positive: $0 < \mathrm{oriented\_coeff}(c,e)$.
background
This 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}$. Chains live in the free $\mathbb{Z}$-module on actual singular $1$-simplices of TopCat.sphere 1.
The raw coefficient of an edge $e$ in a free chain $c$ is the Finsupp evaluation $c(e)\in\mathbb{Z}$. Support membership is exactly nonzero coefficient. Orientation-from-coefficient sends positive integers to forward and non-positive to backward. The oriented coefficient then keeps the raw value on forward and negates it on backward, so it is designed to be the absolute value of a nonzero coefficient.
The local goal is bookkeeping for directed edge flows: once an edge appears in support, one may treat it as positively weighted in its sign-selected orientation.
proof idea
From support membership and mem_edgeSupport_iff, the raw edge coefficient is nonzero. Unfold orientedCoeff and orientationOfCoeff. Case on whether the raw coefficient is positive.
If it is, the orientation is forward, so the oriented coefficient equals the raw coefficient and is positive by the case hypothesis (simp).
If not, simp reduces the oriented coefficient to the negation of the raw value; nonzero plus non-positive forces the raw coefficient negative (omega), hence its negation is positive (omega).
why it matters
In the circle-winding chain development, free $1$-chains are treated as integer flows on singular edges. Positivity of the oriented coefficient on support is the elementary sign-normalization step that lets later arguments sum absolute weights, build oriented boundary contributions, or compare flows without tracking two sign cases at every edge.
The module's headline results are simplexDisplacement and the kills-boundaries identity simplexDisplacement_boundary, which with the fundamental-loop winding give a left inverse to the fundamental class (split-injectivity of $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$). This lemma is local infrastructure for that chain-level bookkeeping rather than a forcing-chain (T0–T8) step.
No downstream uses are recorded yet in the graph; the declaration closes a small positivity gap needed wherever oriented edge coefficients are preferred to raw signed Finsupp values. Surjectivity of the integer comparison (generation of $H_1$) remains open pending a simplicial prism/subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.