Affine origin and deck freedom

For every small type $E$ and reading $r:E\to\mathbb R$, define $O_a(r)(e)=r(e)+a$ for a real offset $a$, define $D_k(r)(e)=r(e)+k\,2\pi$ for an integer turn $k$, define the phase by $\theta_r(e)=\operatorname{Circle.exp}(r(e))$, and define $e\prec_r f$ by $r(e)<r(f)$. The theorem asserts all nine conjuncts: $O_0(r)=r$; for all $a,b\in\mathbb R$, $O_{a+b}(r)=O_a(O_b(r))$; for every $a,e,f$, both $O_a(r)(f)-O_a(r)(e)=r(f)-r(e)$ and $e\prec_{O_a(r)}f\iff e\prec_r f$; if $E$ is nonempty and $r,s:E\to\mathbb R$ have exactly the same increments, meaning $s(f)-s(e)=r(f)-r(e)$ for every ordered pair $e,f\in E$, then there exists exactly one $a\in\mathbb R$ such that $s=O_a(r)$ as functions; $D_0(r)=r$; for all $k,\ell\in\mathbb Z$, $D_{k+\ell}(r)=D_k(D_\ell(r))$; for every $k,e$, $\theta_{D_k(r)}(e)=\theta_r(e)$; for every $k,e,f$, $e\prec_{D_k(r)}f\iff e\prec_r f$; and, if $E$ is nonempty, $D_k(r)=r\iff k=0$. Clauses without a nonemptiness premise also quantify over the empty type; in particular, equality of two readings on an empty event type is automatic, while the two clauses whose claimed uniqueness or faithfulness would be affected explicitly require $E$ to be nonempty.