$\zeta$ has no zeros in the low-lying rectangle $0<\operatorname{Re} s<1$, $|\operatorname{Im} s|\le 2$

Let $\zeta$ denote the Riemann zeta function. The assertion is an unconditional, completely explicit zero-free region for the low-lying part of the critical strip:

In particular $\zeta$ does not vanish anywhere on the real segment $(0,1)$, nor at any point of the critical line of height at most $2$; the first nontrivial zero occurs at height $\approx 14.13$, so the statement is a (modest) truncation of the region where zeros must be searched for.

The statement is provable from the standard theory of the completed zeta function. Write $\Lambda(s)=\pi^{-s/2}\Gamma(s/2)\zeta(s)$ for the completed zeta function and $\Lambda_0(s)=\Lambda(s)+\frac1s+\frac{1}{1-s}$ for its entire part, which is the Mellin transform of the modified Jacobi theta kernel. Because the theta kernel decays like $e^{-\pi t}$, one obtains a completely explicit bound of the form $\|\Lambda_0(s)\|\le \tfrac18$ valid throughout the strip $0<\operatorname{Re} s<1$, whereas the pole terms satisfy

in the rectangle. Hence $\Lambda(s)=\Lambda_0(s)-\frac1s-\frac{1}{1-s}$ cannot vanish there, and since $\pi^{-s/2}\Gamma(s/2)\neq 0$ for $\operatorname{Re} s>0$, neither can $\zeta(s)$.

Formalization note. riemannZeta is Mathlib's zeta function; |s.im| is the absolute value of the imaginary part of $s$.