orientationOfCoeff
plain-language theorem explainer
Maps an integer chain coefficient to a traversal direction: positive means forward, non-positive means backward. Anyone reading singular 1-edges of a free chain with a consistent orientation cites this. The body is a one-line sign case-split into the two constructors of the orientation type.
Claim. Given an integer coefficient $n\in\mathbb{Z}$, return the edge orientation that is forward when $n>0$ and backward when $n\le 0$.
background
The 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}$. Free 1-chains carry integer coefficients on singular edges; to treat a flow as a directed walk one must pick a traversal sense for each supported edge.
EdgeOrientation is the two-value inductive type with constructors forward and backward. Backward stands for the negative of the raw singular edge. This definition turns the sign of a coefficient into that choice, so later constructions can always work with a non-negative reading of the edge.
proof idea
Pure definition: case on whether $0<n$. If yes, return forward; otherwise return backward. No lemmas, no tactics beyond the if expression.
why it matters
Local plumbing for oriented edge reading in the circle winding chain. Downstream, orientedEdgeOfCoeff packages a singular edge with this orientation; orientedCoeff returns the absolute coefficient in that orientation; and positivity lemmas (orientedCoeff_pos_of_mem_edgeSupport, edgeContribution_pos_at_oriented_terminal, initial_eq_of_negative_edgeContribution) use the sign-selected orientation to force compensating outgoing edges in balanced flows. That local positivity is part of the chain-level bookkeeping that supports the winding homomorphism on 1-cycles (the left inverse to the fundamental class). It does not itself touch T0–T8 or the RCL; it sits in the singular-homology half of the foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.