A function \(f\colon \mathbb {R}\to \mathbb {R}\) is càdlàg on \([0,1]\) if it is right-continuous at every \(t\in [0,1)\) and has a left limit at every \(t\in (0,1]\). The Skorokhod space is formalized as the structure Skoro: an honest function on all of \(\mathbb {R}\) that is càdlàg on \([0,1]\), carries an explicit boundedness witness on \([0,1]\) (automatic for càdlàg paths, but bundled so the sups in the metric are genuine reals), and is flat outside \([0,1]\) — constant \(=f(0)\) on \((-\infty ,0]\) and constant \(=f(1)\) on \([1,\infty )\). The flat encoding keeps the usual topology of \(\mathbb {R}\) on the source and makes \(d^\circ (f,g)=0\) imply equality on the nose, so no quotient is needed.

A time change is a structure bundling a map \(\lambda \colon \mathbb {R}\to \mathbb {R}\) that on \([0,1]\) is a strictly increasing continuous bijection fixing \(0\) and \(1\), and is flat outside \([0,1]\) (matching the path encoding of Definition 6.1). Its log-slope norm \(\| \lambda \| ^\circ \) is the supremum of \(\bigl|\log \frac{\lambda t-\lambda s}{t-s}\bigr|\) over \(0\le s{\lt}t\le 1\), and FiniteNorm records that this set of log-slopes is bounded above (the class \(\Lambda ^\circ \)). Composition TimeChange.comp and the inverse TimeChange.symm (via Set.invFunOn) are provided in place of a literal group instance.

For \(f,g\colon \mathbb {R}\to \mathbb {R}\), \(\operatorname {supDiff}(f,g)\) is the supremum of \(|f(t)-g(t)|\) over \(t\in [0,1]\). Billingsley’s metric is \(d^\circ (f,g)=\inf _{\lambda }\max \bigl(\| \lambda \| ^\circ ,\; \operatorname {supDiff}(f\circ \lambda ,\, g)\bigr)\), the infimum running over time changes \(\lambda \) of finite log-slope norm. This is the \(J_1\)-metric whose Cauchy sequences are well behaved (unlike the more elementary \(J_1\) metric with \(\sup _t|\lambda t-t|\) in place of \(\| \lambda \| ^\circ \)).