Measurable branch data for the excursion coupling exists

Let $\mu\perp\nu$ be mutually singular Borel probability measures on $\mathbb R$. Then the adjacent increasing/decreasing crossing pairs of $\mathrm{Graph}^*F_\sigma$ admit a measurable enumeration: there exists a family of measurable branch maps $h\mapsto(\mathrm{source}_i(h),\mathrm{target}_i(h))$, indexed by $i\in\mathbb N$ and defined on measurable sets of active levels, such that at almost every nonzero level $h$

• every active index produces an adjacent increasing/decreasing pair at height $h$,
• every increasing point at height $h$ is $\mathrm{source}_i(h)$ for exactly one active $i$,
• every decreasing point at height $h$ is $\mathrm{target}_i(h)$ for exactly one active $i$, and
• only finitely many indices are active at $h$.

This is the measurable-selection content hidden in Juillet's phrase "choose uniformly among the pairs at level $H$": Proposition 3.2 says that at almost every nonzero level the crossings are finite in number and pair off canonically (the $k$-th increasing crossing with the adjacent decreasing one), and the assertion here is that this canonical pairing can be realised by countably many measurable functions of the level, so that the resulting coupling is a genuine Borel measure.

Formalization note. The conclusion is Nonempty (JuilletPairingData μ ν), the platform structure bundling exactly the four properties above together with the measurability of the branch maps and of the active sets.