EdgeOrientation
plain-language theorem explainer
Two-valued orientation tag for a singular 1-simplex appearing in a directed walk on S¹: forward or backward. Backward means the walk traverses the opposite of the raw singular edge (its formal negative in the chain group). Used throughout the oriented closed-walk extraction that decomposes 1-cycles. Pure inductive definition with decidable equality; no proof content.
Claim. An edge orientation is either $\mathrm{forward}$ or $\mathrm{backward}$. Backward orientation on a singular $1$-simplex $e$ stands for the formal negative $-e$ in the free singular chain group, i.e. traversal of $e$ against its parametrization.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\partial_0 F)-\mathrm{disp}(\partial_1 F)+\mathrm{disp}(\partial_2 F)=0$. Combined with the fact that the once-around generator has winding $1$, this yields a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$.
Singular $1$-chains are free $\mathbb{Z}$-linear combinations of continuous maps $\Delta^1\to S^1$. When extracting closed walks from a cycle, each supported edge may appear with a positive or negative coefficient. The orientation tag records which way the walk should traverse that edge: forward follows the simplex parametrization; backward follows the opposite path and contributes the negative of the raw edge to the chain.
This is bookkeeping for the oriented cyclic-family machinery, not a topological invariant by itself.
proof idea
No proof: an inductive type with two nullary constructors, forward and backward, deriving DecidableEq. The mathematical content is entirely in the doc-comment convention that backward means the formal negative of the raw singular edge.
why it matters
Feeds the oriented closed-walk layer that turns the winding homomorphism into an extraction/decomposition tool for singular $1$-cycles. Downstream, orientationOfCoeff maps the sign of an integer coefficient to this tag; OrientedSingularEdge pairs a singular edge with an orientation; OrientedCyclicFamilyTerm is a finite sign-oriented closed walk built from those pairs. The large-support uniform-oriented extraction steps (largeSupportUniformOrientedExtractionStep, scaled variant) require uniform orientation along the extracted cyclic piece so the older one-scalar cyclic-edge-list interface can consume the newer oriented machinery.
In the broader Recognition story this sits inside the chain-level half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding kills boundaries and hits the generator, while generation (every cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator Mathlib does not yet supply. The orientation tag is the discrete sign data that lets support-decreasing extraction respect that homology picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.