orientedCoeff
plain-language theorem explainer
For a free singular 1-chain on S¹ and a singular 1-simplex, this returns the edge coefficient read in the orientation selected by its sign: positive coeffs stay as-is, negative coeffs are negated. Anyone working with oriented edge supports or flow-style 1-chains on the circle cites it. The body is a two-branch match on the sign-selected orientation.
Claim. Given a free singular $1$-chain $c$ on $S^1$ and a singular $1$-simplex $e$, let $n$ be the integer coefficient of $e$ in $c$. The oriented coefficient is $n$ if $n>0$, and $-n$ otherwise (so it is the absolute value of the coefficient when the edge is traversed in the orientation suggested by $\mathrm{sign}(n)$).
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, aiming at the chain-level fact that winding kills boundaries and hence induces a homology invariant. Singular 1-simplices are the actual 1-simplices of the singular simplicial set of TopCat.sphere 1; free singular 1-chains are the free $\mathbb{Z}$-module on those simplices.
The raw coefficient of an edge $e$ in a chain $c$ is just the evaluation of the free-module function at $e$. Orientation-from-coefficient sends a positive integer to the forward traversal and a non-positive integer to the backward traversal. This definition re-reads that coefficient after flipping when the chosen orientation is backward, so supported edges carry a positive integer in their sign-selected orientation.
Locally this sits in the explicit free $C_1$ bookkeeping used to compare winding against the fundamental class of $S^1$, the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
Definitional, not a proof. Evaluate the raw edge coefficient, pass it to the sign-to-orientation map, and match: on forward return the coefficient unchanged; on backward return its negation. Equivalent to taking the absolute value of the coefficient once the edge is oriented by $\mathrm{sign}(n)$.
why it matters
Needed so that edge supports can be treated as positively weighted oriented edges rather than signed free-module data. The immediate consumer is the positivity lemma: every edge in the support of a free 1-chain has strictly positive oriented coefficient. That positivity is the natural language for flow-style or oriented-support arguments on singular 1-chains while building the winding homomorphism that is a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$).
It does not itself touch the generation/surjectivity half, which the module doc leaves open pending a simplicial prism or subdivision operator. Within Recognition Science this is pure foundation topology supporting the circle winding invariant, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.