Backlund's explicit bound for $N(T)$, $T>2$

Write $N(T)$ for the number of zeros $\rho$ of the Riemann zeta function $\zeta(s)$ with $0<\operatorname{Re}\rho<1$ and $0<\operatorname{Im}\rho\le T$, counted with multiplicity. Backlund's explicit bound states that for every real $T>2$,

This makes the error term in the Riemann–von Mangoldt formula fully explicit, with numerical constants, and in particular implies the formula itself.

Formalization Note The source PDF prints the constant inside the bracket as $-\tfrac78$. Backlund's theorem and the standard literature (e.g. Titchmarsh, Ch. 9, and Hasanalizade–Shen–Wong 2022) have $+\tfrac78$, matching the expansion $N(T)=\frac{T}{2\pi}\log\frac{T}{2\pi}-\frac{T}{2\pi}+\frac78+S(T)+O(1/T)$; this draft uses $+\tfrac78$. The decimal constants are exact rationals (0.137 = 137/1000, etc.). $N(T)$ is zetaZeroCount T.