Principal ledger reconstruction

For every small type $E$, real cut $c$, reading $r:E\to\mathbb R$, and event $e\in E$, let $P_c(r(e))$ be the representative of $r(e)$ modulo $2\pi$ in $(c,c+2\pi]$, and let $Q_c(r(e))\in\mathbb Z$ be its associated quotient, so the custom reconstructed value is $P_c(r(e))+Q_c(r(e))\,2\pi$; also, the custom principal edge turn at base $b$ and difference $d$ is the negative of the quotient obtained by reducing $b+d$ into $(b-\pi,b+\pi]$. The theorem asserts four conjuncts: $c<P_c(r(e))$ and $P_c(r(e))\le c+2\pi$; $P_c(r(e))+Q_c(r(e))\,2\pi=r(e)$; for every pair of real cuts $c_1,c_2$, both reconstructed values are equal and $\operatorname{Circle.exp}(P_{c_1}(r(e)))=\operatorname{Circle.exp}(P_{c_2}(r(e)))$; and $Q_{-\pi}(r(e))$ equals the negative of the principal edge turn at base $0$ and difference $r(e)$, which after expanding that custom definition is $Q_{-\pi}(r(e))=-(-Q_{-\pi}(r(e)))$. All clauses quantify over arbitrary cuts and readings; when $E$ is empty, their additional quantification over $e\in E$ makes them vacuous.