A Computation-Free Spectral Improvement to the Montgomery–Taylor Bound for Simple Critical Zeros

Let N(T) count the nontrivial zeros of the Riemann zeta function with 0 < Im ρ ≤ T, including multiplicity, and let N₀,ₛ(T) count those zeros that are both simple and on the critical line in the same range. This paper proves unconditionally that there is a constant δ > 0 such thatliminf as T → ∞ of N₀,ₛ(T)/N(T) is at least 3/2 − (1/√2) cot(1/√2) + δ.Thus the optimized Montgomery–Taylor constant 0.672500703679411… is not the endpoint of the unconditional finite-compression method. The proof retains a nonnegative clipped spectral deviation of the Gram matrix of the simple-zero sampling vectors. Three consecutive translates force a positive contribution because the positive zero set of the Montgomery–Taylor kernel is sum-free. Compactness and Lamzouri’s smooth-cutoff approximation turn this qualitative obstruction into a fixed spectral gain, while a three-residue partition handles arbitrary gaps using only their total span.The argument is analytic and uses no numerical optimization, interval certificate, or generated finite-range candidate. The deposit includes a standalone Lean 4 formalization of the new finite-dimensional, kernel, pinching, combinatorial, and asymptotic deductions. Published pair-correlation and Riemann–von Mangoldt inputs are represented by explicit interfaces rather than re-proved from first principles.