montgomery_odlyzko_law

⚠️ 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-Odlyzko law: The distribution of normalized spacings between consecutive zeros of ζ(s) follows the GUE eigenvalue distribution 1-(sin(πx)/(πx))². The pair correlation was proved by Montgomery; the full level spacing distribution (all k-point correlations) matching GUE is the conjecture.

Why this node was retired

The posted statement is

import Mathlib

theorem montgomery_odlyzko_law :
    ∀ alpha beta : ℝ, alpha ≤ beta →
    ∃ (zeros : ℕ → ℝ) (hpos : ∀ n, 0 < zeros n)
      (hincr : StrictMono zeros),
      Filter.Tendsto (fun T : ℝ =>
        (∑ n ∈ Finset.range (Nat.floor T),
          if alpha * Real.log T / (2 * Real.pi) ≤ zeros n ∧
             zeros n ≤ beta * Real.log T / (2 * Real.pi)
          then 1 else 0 : ℝ) / Real.log T)
      Filter.atTop
      (nhds (∫ x in Set.Ioo 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.