montgomery_pair_correlation

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Montgomery's pair correlation conjecture (1973): The pair correlation of imaginary parts of zeros of ζ(s) follows the GUE random matrix distribution 1 - (sin(πx)/(πx))². Confirmed numerically; connection to random matrix theory discovered by Montgomery–Dyson (1972).

Why this node was retired

The posted statement is

import Mathlib

theorem montgomery_pair_correlation :
    ∀ alpha beta : ℝ, alpha ≤ beta →
    ∃ (gammas : ℕ → ℝ),
      (∀ n, 0 < gammas n) ∧
      Filter.Tendsto (fun T : ℝ =>
        (1 / Real.log T) * ∑ n ∈ Finset.Icc 1 (Nat.floor T),
          if alpha ≤ gammas n * Real.log T / (2 * Real.pi) ∧
             gammas n * Real.log T / (2 * Real.pi) ≤ beta
          then 1 else 0)
      Filter.atTop (nhds (∫ x in alpha..beta,
        1 - (Real.sin (Real.pi * x) / (Real.pi * x))^2)) := by
  sorry

The formula counts individual positive ordinates in a possibly negative window instead of normalized signed differences of pairs of zeta-zero ordinates; the sequence is also not tied to zeta zeros.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Use the actual nontrivial zeta zeros (with the intended RH hypothesis if needed), and count ordered distinct pairs via (log T)/(2π)·(γ−γ′), with the source normalization by the number of zeros up to T. State the limiting pair-correlation measure including the diagonal convention.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.