Theorem: Serial path certificate and excursion profile

The serial composition of (eq:weaksteps) along the path to $v$ is exactly

Define its depth predictor

Then

The exact returned-code error is

Its linearly interpolated preorder profile, with terminal value zero appended, converges in distribution in the uniform topology to

Furthermore,

Proof. Lemma lem:depolarizing makes the parameters multiply, yielding the exact composition. The function $x\mapsto e^{-x}$ is one-Lipschitz on $[0,\infty )$. Therefore Lemma lem:depolarizing and Theorem thm:path prove (eq:serialcomparison).

Uniform approximation by the depth predictor, together with (eq:coding), gives (eq:serialprofile) by continuous mapping. Appending the last zero is harmless because the normalized last height tends to zero and the uniform approximation controls the corresponding label sum. Uniform convergence in distribution to a continuous profile also gives convergence of the Riemann sums. Removing the root and using $N-1$ instead of $N$ changes a bounded average by $O(N^{-1})$, proving (eq:serialintegral).