The completed-graph occupation measure charges only the paired routes

Let $\mu,\nu$ be Borel measures on $\mathbf{R}$ and let data be measurable branch data for Juillet's completed-graph construction (a JuilletPairingData). Then the associated occupation measure

is concentrated on the set $\Gamma$ of paired routes:

Why this is the remaining content. The pointwise inclusion is immediate: pairedAtLevel F h ⊆ pairedRoutes F for every $h$, since pairedRoutes is by definition the union of pairedAtLevel over levels, so the level $h$ itself is the required witness. The field paired_ae of the branch data says precisely that for Lebesgue-almost every level $h$ and every index $i$ with $h \in \mathrm{active}_i$, the pair $(\mathrm{source}_i(h), \mathrm{target}_i(h))$ lies in pairedAtLevel F h. Hence for each $i$ the bad level set $\{h \in \mathrm{active}_i : (\mathrm{source}_i(h), \mathrm{target}_i(h)) \notin \Gamma\}$ is Lebesgue-null, and Measure.sum_apply_eq_zero reduces the claim to the individual summands.

The genuine difficulty is that this last reduction passes through a pushforward: Measure.map is an outer measure, and only the inequality $\mu(f^{-1}(s)) \le (f_{\#}\mu)(s)$ holds for a general set $s$. Since $\Gamma$ is not known to be Borel — regularLevel quantifies existentially over finite increasing enumerations of the level set — one cannot simply transfer the null preimage through the map. Closing the statement therefore requires either establishing measurability of pairedRoutes, or exhibiting a measurable set $S \subseteq \Gamma$ carrying almost every image point.

Formalization Note The measure of $\Gamma^{c}$ is understood in the usual Mathlib sense, i.e. via the outer measure, so the statement is meaningful without assuming $\Gamma$ measurable.