Part II: Number-Theoretic & Analytic Bridge for riemann_744

This file develops the number-theoretic and real-analytic bridge between the elementary Matiyasevich–Aaronson counterexample predicate MatiyasevichRiemannCounterexample (computed by riemann.nql) and Mathlib's RiemannHypothesis.

Mathematical Overview

For each integer $x > 253$ and $L_x = \operatorname{lcm}(1, \dots, x)$, the NQL program tests whether $$H_{L_x} > x \quad\text{and}\quad (H_{L_x} - x)^2 > x \cdot H_x^4.$$ We decompose the equivalence $$\left(\exists x : \mathbb{N},; \text{MatiyasevichRiemannCounterexample } x\right) \iff \neg \text{RiemannHypothesis}$$ into the following steps, proving all elementary, harmonic, Euler–Mascheroni, and Chebyshev-$\psi$ reductions completely in Lean 4 and isolating the classical complex-analytic number theory results of Schoenfeld (1976) and Schmidt (1903):

Rational and Real Reformulations:

matiyasevichRiemannCounterexample_iff_harmonic: equivalence with the $\mathbb{Q}$-inequality.

matiyasevichRiemannCounterexample_iff_real: equivalence with the $\mathbb{R}$-inequality.

matiyasevichRiemannCounterexample_iff_sqrt_lt: single real inequality $253 < x ;\wedge; \sqrt{x} \cdot H_x^2 < H_{\operatorname{lcm}(1,\dots,x)} - x$.

matiyasevichRiemannCounterexample_iff_abs_and_sqrt_lt: formulation with $|H_{\operatorname{lcm}(1,\dots,x)} - x| = H_{\operatorname{lcm}(1,\dots,x)} - x$.

Identity $\psi(x) = \log \operatorname{lcm}(1, \dots, x)$ and Positivity of lcmUpTo:

lcmUpTo_pos, one_le_lcmUpTo, dvd_lcmUpTo, self_le_lcmUpTo, lcmUpTo_mono.

psi_eq_log_lcmUpTo : Chebyshev.psi x = Real.log (lcmUpTo x) and exp_psi_eq_lcmUpTo : Real.exp (Chebyshev.psi x) = lcmUpTo x.

Euler–Mascheroni & Harmonic-to-Chebyshev-$\psi$ Bounds:

$\psi(x) + \gamma < H_{\operatorname{lcm}(1,\dots,x)} \le \psi(x) + 1$ (psi_add_eulerMascheroniConstant_lt_harmonic_lcmUpTo, harmonic_lcmUpTo_le_psi_add_one).

$\log x \le H_x \le 1 + \log x$ and $(\log x)^2 \le H_x^2 \le (1 + \log x)^2$.

Elementary Reduction Between $\psi(x)$ Bounds and MatiyasevichRiemannCounterexample:

not_matiyasevichRiemannCounterexample_of_psi_sub_le: proves that Schoenfeld's explicit bound $\psi(x) - x \le \frac{1}{8\pi}\sqrt{x}(\log x)^2$ implies $\neg \text{MatiyasevichRiemannCounterexample } x$ (absorbing the $+1$ harmonic slack via $\pi > 3$ and $x > 253$).

matiyasevichRiemannCounterexample_of_sqrt_mul_harmonic_sq_le_psi_sub and matiyasevichRiemannCounterexample_of_sqrt_mul_one_add_log_sq_le_psi_sub: proves that a sufficiently large positive excursion of $\psi(x) - x$ yields MatiyasevichRiemannCounterexample x.

Classical Analytic Number Theory Ingredients (Schoenfeld 1976 & Schmidt 1903):

riemannHypothesis_imp_schoenfeld_psi_bound: under RiemannHypothesis, $|\psi(x) - x| \le \frac{1}{8\pi} \sqrt{x} (\log x)^2$ for $x > 253$.

not_riemannHypothesis_imp_exists_psi_oscillation: under ¬ RiemannHypothesis, there exists $x > 253$ with $\sqrt{x} H_x^2 \le \psi(x) - x + \gamma$.

1. The Matiyasevich–Aaronson Elementary Counterexample Predicate