The Montgomery–Taylor constant is less than 1.3275

The single numerical input to both headline bounds. Since (1/√2)² = 1/2 exactly, the values cos(1/√2) and √2 sin(1/√2) are alternating series with rational terms, so bounding them needs no estimate at an irrational argument: five terms bound the first from above, four bound the second from below, and the gap to 1.3275 is about 7 · 10⁻⁷.

noncomputable def ZetaZeros.montgomeryTaylorConst : ℝ

The Montgomery–Taylor constant 1/2 + (1/√2) cot(1/√2) = 1.3274992963….

Equations

• ZetaZeros.montgomeryTaylorConst = 1 / 2 + 1 / √2 * (1 / √2).cot

noncomputable def ZetaZeros.simpleProportion : ℝ

The proportion of zeros shown simple and on the critical line, 3/2 - (1/√2) cot(1/√2) = 0.6725007037….

Equations

• ZetaZeros.simpleProportion = 3 / 2 - 1 / √2 * (1 / √2).cot

noncomputable def ZetaZeros.distinctProportion : ℝ

The proportion of zeros shown distinct, 5/4 - (1/(2√2)) cot(1/√2) = 0.8362503518….

Equations

• ZetaZeros.distinctProportion = 5 / 4 - 1 / (2 * √2) * (1 / √2).cot

theorem ZetaZeros.sin_inv_sqrt_two_pos : 0 < Real.sin (1 / √2)

sin(1/√2) > 0.

noncomputable def ZetaZeros.cosTerm (k : ℕ) : ℝ

The k-th term of the rational series for cos(1/√2).

Equations

• ZetaZeros.cosTerm k = 1 / (2 ^ k * ↑(2 * k).factorial)

noncomputable def ZetaZeros.sinTerm (k : ℕ) : ℝ

The k-th term of the rational series for √2 sin(1/√2).

Equations

• ZetaZeros.sinTerm k = 1 / (2 ^ k * ↑(2 * k + 1).factorial)

theorem ZetaZeros.hasSum_cosTerm : HasSum (fun (k : ℕ) => (-1) ^ k * cosTerm k) (Real.cos (1 / √2))

cos(1/√2) is the alternating sum of 1 / (2ᵏ (2k)!).

theorem ZetaZeros.hasSum_sinTerm : HasSum (fun (k : ℕ) => (-1) ^ k * sinTerm k) (√2 * Real.sin (1 / √2))

√2 sin(1/√2) is the alternating sum of 1 / (2ᵏ (2k+1)!).

theorem ZetaZeros.cos_inv_sqrt_two_lt : Real.cos (1 / √2) < 0.7602447

Five terms bound cos(1/√2) from above. The partial sum is 0.760244605….

theorem ZetaZeros.sqrt_two_mul_sin_inv_sqrt_two_gt : 0.9187251 < √2 * Real.sin (1 / √2)

Four terms bound √2 sin(1/√2) from below. The partial sum is 0.918725198….

theorem ZetaZeros.inv_sqrt_two_mul_cot_lt : 1 / √2 * (1 / √2).cot < 0.8275

(1/√2) cot(1/√2) < 0.8275.

theorem ZetaZeros.montgomeryTaylorConst_lt : montgomeryTaylorConst < 1.3275

The numerical input. C_MT < 1.3275, which is exactly what both headline bounds need: 2 - 1.3275 = 0.6725 and 3/2 - 1.3275/2 = 0.83625.

theorem ZetaZeros.simpleProportion_eq : simpleProportion = 2 - montgomeryTaylorConst

C₀ = 2 - C_MT.

theorem ZetaZeros.distinctProportion_eq : distinctProportion = 3 / 2 - montgomeryTaylorConst / 2

C₁ = 3/2 - C_MT/2.