Definition. Polygonal walks and their mutual signed intersection [cn-0069]

A polygonal walk \(\gamma =(e_1,\ldots ,e_r)\) in the plane is a finite ordered sequence of directed straight-segment traversals, with the end of each traversal equal to the start of the next. It is closed if its final endpoint equals its initial endpoint. Stationary steps can be omitted. Different portions of the walk may meet or cross, and a segment may be traversed more than once. Each traversal retains its position in the sequence and its direction.

Let \(\gamma =(e_1,\ldots ,e_r)\) and \(\eta =(f_1,\ldots ,f_s)\) be two such walks. Assume every meeting between them is transverse and away from all segment endpoints. For a pair of traversals, set \(I(e_i,f_j)=0\) if they are disjoint; at a crossing set it equal to the sign of the determinant of their two directed segment vectors, in the order \(e_i,f_j\). This is the same sign convention [cn-0010] used for graph edges. Their mutual signed intersection is

\[I(\gamma ,\eta )=\sum _{i=1}^{r}\sum _{j=1}^{s}I(e_i,f_j).\]

The sum has one term for each pair of traversals, one from each walk. A crossing between two portions of \(\gamma \) alone, or between two portions of \(\eta \) alone, is not included. If \(\eta \) passes through a crossing of two portions of \(\gamma \), both pairings with \(\eta \) are included, with their respective signs. Similarly, traversing a segment twice in the same direction counts its intersections with the other walk twice. The closed-walk lemma [cn-0015] states that this mutual sum is zero when both walks are closed.

Proof dependencies
None.
Provenance
OpenAI, 23 September 2026 [cn-0042], final topological step in the proof of Lemma 3.1; notation and multiplicities made explicit on 9 October 2026. Lean source: PolygonalWalks, definition polygonIntersection.