Proposition 3.2 - almost every level of $F_\sigma$ is regular

Let $\mu\perp\nu$ be mutually singular Borel probability measures on $\mathbf{R}$ and $F_\sigma = F_\mu - F_\nu$. Then for Lebesgue-almost every level $h\neq 0$: the set of generalized solutions of $F_\sigma = h$ is finite with an even number $2n$ of elements; each solution is an increasing or a decreasing point of the completed graph; and, enumerated in increasing order $x_1 < \dots < x_{2n}$, the solutions strictly alternate between increasing and decreasing crossings, with equal numbers $n$ of each, starting with an increasing point when $h > 0$ and with a decreasing point when $h < 0$.

This is the geometric heart of the excursion coupling: at almost every level the completed graph crosses the horizontal line $\mathbf{R}\times\{h\}$ in a finite alternating pattern, which is what makes the pairing of consecutive crossings in eq. (14) well defined.

Formalization Note The conclusion is packaged as the predicate regularLevel: an enumeration $x : \mathrm{Fin}(2n) \to \mathbf{R}$, strictly monotone, with range the level set, each $(x_i,h)$ an increasing or decreasing point, and $(x_i,h)$ increasing iff ($h>0$ iff $i$ is even) for the 0-based index $i$.