Cutoffs exist

The source asks for a smooth even cutoff, valued in [0,1], supported in (-1/2, 1/2) and identically one on |x| ≤ 1/2 - delta. That is exactly Mathlib's ContDiffBump centred at the origin with inner radius 1/2 - delta and outer radius 1/2: the bump is radial, so evenness comes free from ContDiffBump.neg, and the two radius conditions are what 0 < delta < 1/4 supplies.

theorem ZetaZeros.exists_isCutoff {delta : ℝ} (h0 : 0 < delta) (h4 : delta < 1 / 4) : ∃ (psi : ℝ → ℝ), IsCutoff delta psi

Cutoffs exist.