Orientation reversal of the lifted clock

For every small type $E$, reading $r:E\to\mathbb R$, events $e,f\in E$, and integer $k$, define the reversed reading by $R(r)(e)=-r(e)$, the deck shift by $D_k(r)(e)=r(e)+k\,2\pi$, the phase by $\theta_r(e)=\operatorname{Circle.exp}(r(e))$, and $e\prec_r f$ by $r(e)<r(f)$. The theorem asserts the conjunction $\theta_{R(r)}(e)=\theta_r(e)^{-1}$, $e\prec_{R(r)}f\iff f\prec_r e$, and $R(D_k(r))=D_{-k}(R(r))$ as equality of functions $E\to\mathbb R$. These statements quantify over every $E$, including the empty type, in which the eventwise assertions and function equality are vacuous.