2026-10-02 · article Riemann hypothesisWeil explicit formulatime–band limiting

The Riemann hypothesis — the sunk eigenvalues of the Weil quadratic form can be counted from below without assuming the Riemann hypothesis

Leanmachine-checked (Lean 4 + mathlib, 0 sorry, no native_decide, axioms a subset of propext, Classical.choice, Quot.sound; theorem names given) paperproved, not yet machine-checked computationchecked on this machine, within the range stated; not a claim made to the outside knowna known theorem, a restatement, or a check of the literature

This page claims nothing about the Riemann hypothesis itself. What it treats is the counting of the spectrum of a quadratic form truncated to test functions with compact support. The main result (the lower bound on the number of sunk eigenvalues) never uses whether the zeros lie on the critical line, and so whether it holds or not, nothing comes back about where the zeros are. The reasons are given in §11.

Do all the non-trivial zeros ρ of the Riemann zeta function ζ(s) have real part 1/2?
(The non-trivial zeros lie in the strip 0 < Re s < 1; writing ρ = 1/2 + iγ, the conjecture is the same as "every γ is real".)

The restatement this article uses is Weil's criterion. Let f be a real-valued even function and F its Fourier transform; the explicit formula rewrites the sum over zeros Σρ F(γρ)2 as the sum of three terms — the pole, the Archimedean place (the gamma factor), and the prime powers. If the Riemann hypothesis is true, γρ is real and so is F(γ), so the left-hand side is non-negative as a sum of squares. Conversely, if this quadratic form is non-negative on a sufficiently wide family of test functions, the Riemann hypothesis follows (Weil). known

The difficulty lies in the prime term on the right. The pole and Archimedean terms can be handled analytically, but the prime term is arithmetic itself — which log k each Λ(k) (the von Mangoldt function) sits on — and it is this arrangement that supports non-negativity. Restrict the support of the test functions to [−L, L], and the prime term becomes a finite sum over k ≤ e2L; the problem fits inside a finite window. As long as the window is finite, only the zeros up to height about 2πe2L are visible.

So that there are about e2L sunk eigenvalues is itself known, and the content of this article lies beyond that — a theorem bounding their number from below, the fact that this bound does not need the Riemann hypothesis, and measurements of where the slack lives.

Work through Li's criterion by computation, and the slack in the positivity of λn checks only the density of the zeros — even a synthetic sequence of zeros built from the counting function alone reproduces the true λn to within 0.75% at n = 199. Move then to the Weil quadratic form WL, which has the freedom of "in which direction is the slack smallest", and it passes the same checkpoint — merely rearranging Λ(k) onto other prime powers, as the same multiset of values, breaks positivity. Take the whole spectrum of WL, and the number of sunk eigenvalues closely follows a parameter-free formula, n(L) = Sh(T*) − N(T*) = e2L − 7/8 − S(T*) (Sh is the Shannon number of the window, N the zero-counting function). A theorem bounding this number from below (Theorem A) was set up using the trace of the time–band operator in place of Landau's dimension theorem; to bring the u-dependence of the bound down from 1/u to log(1/u), the 1/k law for the traces was derived by a cluster expansion; and the cost of zeros off the critical line was controlled by a transfer inequality via Phragmén–Lindelöf. The Riemann hypothesis is assumed nowhere. Zeros off the critical line enter only the transfer constant κ, and their contribution is small compared with the main term e2L. At L = 2 with threshold 10−3: paper lower bound 45.24, 46.4 with one measured input, measured count 53.

f        real, even, support ⊂ [−L, L], an L² function. F(z) = ∫ f(t) e^{izt} dt (an entire function of exponential type L)
h = F²,  g = f * f (support ⊂ [−2L, 2L])
W_L[f] = Σ_ρ F(γ_ρ)²,   γ_ρ := (ρ − 1/2)/i     (written without using the Riemann hypothesis)
       = h(i/2) + h(−i/2) − g(0) log π + (1/2π) ∫ h(r) Re ψ(1/4 + ir/2) dr − 2 Σ_k Λ(k) k^{−1/2} g(log k)
W_L    = 2aaᵀ − (log π) I + A_L + Q_L    (an m×m real symmetric matrix in the even cosine basis φ_0, …, φ_{m−1})
S_L    = 2aaᵀ − (log π) I + A_L          (pole + Archimedean; the part without primes)
Q_L    = −2 Σ_{k ≤ e^{2L}} Λ(k) k^{−1/2} G(log k)   (the prime-power part)
n(W_L; ε) := sup{ dim V : W_L[f] ≤ ε‖f‖² (∀ f ∈ V)}      (the quantity counted: "the number of sunk eigenvalues")
T*  := 2π e^{2L},   Sh(T) := LT/π,   N(T) = the number of zeros up to height T (with multiplicity)
S(T) := (1/π) arg ζ(1/2 + iT),   N(T) = (T/2π) log(T/2πe) + 7/8 + S(T) + O(1/T)
Q = Q_{L,T}   the time–band operator on the even part (kernel (1/π)[s(x−y) + s(x+y)], s(u) = sin(Tu)/u)
A = P_{[−L,L]} B_{[−T,T]} P,   c := 2LT,   ℓ := log(4LT) + γ_E + 1
a_k := tr(A^k − A^{k+1}),   u_j := 1 − λ_j(Q),   n(u) := #{ j : u_j ≤ u }
𝔇(u) := Sh(T) − #{ j : λ_j(Q) > 1 − u }       (what the time–band operator "misses")
tail_δ(f) := (1/2π) ∫_{|x|>T} |F(x + iδ)|² dx     (the amount leaking outside the band; δ is the offset from the critical line)
Θ(w) := (1/2π) ∫_{|x|>T} F(x + w) F̃(x − w) dx   (an entire function of exponential type 2L; Θ(iδ) = tail_δ(f))
V_u := span{ v_j : 1 − λ_j(Q) ≤ u }               (the subspace sunk to depth u or less)

Λ(k) is the von Mangoldt function. To avoid confusion, ℓ is used for the constant in the traces. The constant term j = 0 of the matrix (the constant function) is always included in the basis.

Even among equivalent criteria, what each one checks differs from criterion to criterion. There is one procedure for seeing it: check whether a fake input that does not use zeta gives the same value. If it does, the slack in that criterion sees only properties that the fake input shares.

① The slack in Li's criterion does not use arithmetic

Build a synthetic sequence of zeros, placed rigidly from the zero-counting function N(T) alone, compute λn from it, and it reproduces the true values to within 0.75% at n = 199. The first n at which λn can detect a pair of zeros off the critical line by δ is n* ≈ (T2/δ) log(n log n) (in a positive control with δ = 0.45, T = γ1, measured n* = 3907 against an envelope prediction of 3855); to see an offset of δ = 0.1 at the height T ≳ 1012 up to which the zeros have been checked, n ≳ 1026 is needed. computation

② The Weil quadratic form passes the same checkpoint

The smallest eigenvalue μ of WL becomes strongly negative merely by placing the prime-power weights Λ(k), as the same collection of values, onto other prime powers. So positivity sees arithmetic — which weight sits on which log k. The true Λ lies just inside the boundary of the positive cone, and that distance μ/‖∇Λμ‖ shrinks rapidly with L. The size at which zeros off the line are detected is proportional to δ2 and almost independent of the height T (Li degrades as T2/δ), but the band of the test functions has to cover the height of the violation (m ≳ TL/π, L ≳ (1/2) log(T/2π)). computation

③ Control: Báez-Duarte's criterion is exponentially blind in the height of the zeros

For ck = Σj≤k (−1)j C(k,j)/ζ(2j+2), "the Riemann hypothesis ⟺ ck ≪ k−3/4+ε" (Báez-Duarte). known Computing to more than 40 digits for k ≤ 104 and subtracting Maślanka's formula, with 7 pairs of zeros the residual falls to 7.9×10−11 of the amplitude of the first pair. computation

Detecting a zero off the line at height γ with real part 1/2 + δ needs log k ≳ (2/δ)(πγ/4 − 9.46) (the source is the e−πγ/4 of the gamma factor), which is worse than Li's polynomial T2/δ. papercomputation In a negative control with the Möbius function rearranged, |ck| k3/4 is 3900 times the coefficient of the true oscillation: the threshold k−3/4 is exactly "the size that random signs produce". computation

Line up all the eigenvalues of WL and no flat step appears; instead there is a bundle sinking toward 0 like a logarithmic staircase (−ln λj is concave in j). The size of that bundle, n(WL; ε), is counted as the number of eigenvalues at or below the threshold ε.

The density of degrees of freedom that the even part of the window can hold is L/π (Sh(T) = LT/π of them up to height T), and the density of zeros that the explicit formula must cancel is (1/2π) log(T/2π). The former is constant and the latter grows, so the difference Sh(T) − N(T) reaches a maximum at some height, and that height is exactly T* = 2πe2L (what Zhu calls the resolution height). Substituting, the 2L cancels and a parameter-free formula remains. paper(as an estimate)

For the smooth part, the position and value of this maximum were closed in Lean. With shannon L T = LT/π and smoothCount T = (T/2π) log(T/2πe) + 7/8:

• LeanTimeBand.crossover_le — if 0 < T then shannon L T − smoothCount T ≤ exp(2L) − 7/8
• LeanTimeBand.crossover_eq — equality at T = 2π exp(2L)
• LeanTimeBand.crossover_lt — strictly smaller for every other T > 0 (the only height giving the maximum is T*)

Each comes down to the elementary inequality t(1 − log t) ≤ 1 (t > 0, equality at t = 1). So −7/8 is not a fitted constant. 7/8 = 1 − 1/8 breaks down into the +1 of the argument principle (the increment of s(s−1)/2) and the −π/8 of the Stirling expansion of the Riemann–Siegel θ (−1/8 as a count), and depends on neither L nor T*. All of the L-dependence is in S(T*). paperknown(the unconditional form of Riemann–von Mangoldt)

Comparison with measurement

These counts were taken with the number of zeros N(T*) counted exactly by PARI/GP's lfunzeros (up to 601 zeros) and with the Galerkin dimension saturated (m ≳ 1.3 Sh(T*)). The count does not depend on the Galerkin dimension m. computation

At threshold 10−3, while the count moves from 1 to 146, the difference from Sh(T*) − N(T*) stays within 0.39–1.46. computation The main term e2L is the same as in the Connes–Consani count ("their number increases roughly like µ", with µ = e2L). known

The formula of §06 is an estimate and a measurement. This section turns it into a theorem, as a bound from below.

Taking T = T*, the main term is e2L − 7/8 − S(T*) (exactly the model of §06). 𝔇(u) is how many functions with "leakage outside the band at most u" the time–band operator misses, and κ is the transfer constant expressing the cost of zeros off the critical line. The Riemann hypothesis is not assumed. Zeros off the critical line appear only in κ. paper

The proof has two steps.

• Step (a): there are many functions with small leakage. Of the eigenvalues of the time–band operator Q on the even part, Sh(T) − 𝔇(u) exceed 1 − u, and every element of the space Vu spanned by their eigenfunctions leaks at most u‖f‖2 outside the band [−T, T] of the Fourier transform.
• Step (b): the conditions for vanishing at the zeros are few. The condition that F vanish at the zeros up to height T is one real condition per zero, so the codimension is at most N(T). For zeros on the line, F being even makes the mirror image vanish automatically; for zeros off the line, the quadruple ρ, 1−ρ, ρ̄, 1−ρ̄ all vanish under 2 real conditions. paper On the remaining space, WL[f] is only the sum over zeros above height T, and that is bounded by the leakage. Finally, turning "the dimension of a subspace on which the form is at most ε" into "the number of eigenvalues at most ε" is finite-dimensional linear algebra.

LeanSunkCount.card_le_of_form_le, SunkCount.card_eigenvalues_le — for a symmetric operator in finite dimensions, if ⟨x, Tx⟩ ≤ ε‖x‖2 on a subspace U with n ≤ dim U + k, then n ≤ #{i : λi ≤ ε} + k.

Part ① — using the trace instead of Landau's dimension theorem

What step (a) needs — "the number of eigenvalues of Q close to 1" — is usually drawn from Landau's dimension theorem. Here it was done with trace computations alone.

Chebyshev's inequality gives #{λj(Q) > 1 − u} ≥ Sh(T) − (1/u)[(1/2π2) log(4LT) + C0]. paper The numerical slope is 0.050387, agreeing with 1/(2π2) = 0.050661 (a regression over 4 octaves). A negative control for scale invariance agreed in all digits. computation

LeanTimeBand.trace_compress_sub_sq (tr(A − A2) is the square of the Hilbert–Schmidt norm of the part that leaks outside the window), TimeBand.card_gt_ge_trace_sub (the Chebyshev counting step) and others. The list is in §13.

Part ② — the 1/k law for the traces, and the cluster expansion

The bound of step (a) acts as 1/u, which as it stands is useless (at L = 2 the number missed is 401–481, and the lower bound is empty). Bringing it down to log(1/u) needs the higher traces ak = tr(Ak − Ak+1). With c → ∞ and k fixed, the leading term is

For k = 1, 2, 3 the constant terms were derived on paper (a1 = ℓ/π2, a2 = ℓ/(2π2), a3 = ℓ/(3π2)), and the even part is exactly half (least-squares slope of a2 0.0253588 against 1/(4π2) = 0.0253303, constant 0.0399 against (γE+1)/(4π2) = 0.0399513; relative 10−11 at c = 3×104). papercomputation

For general k, the starting point is the reduction tr Ak = c/π − Jk/πk, Jk = ∫ min(Mk, c) ∏ sinc (Mk the diameter of k points). k = 3 drops to one dimension by symmetry: J3 = (3/2)∫0∞ min(t, c) ψ(t)/t2 dt, ψ(t) = 2[(1 − cos 2t) Si(2t) − sin 2t · Cin(2t)]. paper

LeanTimeBand.window_length (the length 2L − max(|u|, |v|, |u+v|) of the intersection of the three windows appearing in tr A3), sin_shift_decomp and others.

General k is handled by a cluster expansion. The weight of an arc (cluster) is γ(n) = 21−n, the weight of a cut is Ck,m = C(k, m) 2m−k, and the amplitude of odd clusters is identically 0. The amplitude of even clusters is

v2 = −2 and v4 = 8π2/3 were derived independently on paper; the general form comes from the binomial expansion of the finite Hilbert transform identity k*k = −π2δ + μ (k(u) = 1/(2 sinh(u/2)), μ̂(ξ) = π2 sech2(πξ); Poincaré–Bertrand). paperknown(the identity itself) As a check, v6 = −46π4/15 and v8 = 352π6/105 were confirmed to 15 digits by a quadrature that does not use Fourier. computation

Returning the sum over clusters to ak needs the following combinatorial identity.

LeanTimeBand.binom_oddH_identity (TimeBandTrace3.lean, all k). On paper it takes 5 lines, using On = ∫01 (1 − x2n)/(1 − x2) dx.

From the leading term to a uniform bound — hypothesis (LW∞) and the windowed theorem

The 1/k law is the leading term for c → ∞ with k fixed, not an inequality uniform in all K. Using it in the lower bound needs, for ĉK := π2(tr Q − tr QK+1) − ℓHK,

and this was separated out explicitly as a hypothesis. Theorem A′ uses only one K, so the loss is only 0.0517·C0. paper Measured, ĉK = −HK + C (C = 2.80 ± 0.01, almost independent of c); with C0 = 2.80 the loss is 0.145, and with the measured violation on the even part (≤ 0.07) it is 0.004. computation No closed form for C has been found (7ζ(3)/3 = 2.8042 and π2/4 + 1/3 = 2.8007 both sit at the edge of the measurement range, and neither is asserted).

Theorem C′ (windowed): the total variation of φK(u) = (1 − u)(1 − (1 − u)K) is at most 2 independently of K, so the remainder need only be bounded, not summable. The deep side can be discarded with φK ≤ Ku (its effect on the lower bound at L = 2 is 0.001), and moreover only one side is needed — ĉK ≤ C0 is equivalent to a lower bound on tr QK+1, and that comes from a test subspace (λj(PQP) ≤ λj(Q)). paper

LeanTimeBand.sum_pow_ge_card_mul (if the deficiency on a test subspace is at most u, then tr Qm ≥ (dimension)·(1 − u)m), deep_tail_negligible, abel_remainder_bound and others.

Part ③ — controlling the cost of zeros off the critical line with a transfer inequality

Step (b) said that "the sum over zeros above height T is bounded by the leakage" because, if the zeros are on the line, Σ|γ|>T F(γ)2 is a quantity outside the band. For a zero off the line, γ = x + iδ, one looks at F(x + iδ), and the leakage on the real axis has to be moved to the leakage tailδ(f) translated into the complex plane. The ratio is the transfer constant κ.

Here f is an element of any subspace of the sunk subspace for the band T1 = T − σ. Even at σ = 0, √u comes out unconditionally. The only tool is a one-variable Phragmén–Lindelöf, using that Θ(w) is an entire function of exponential type 2L and that H(w) = Θ(w) e2iLw is bounded in the upper half-plane. e2L|δ| comes from Plancherel and is sharp; the power of u comes from Cauchy–Schwarz; the two separate.paper(Phragmén–Lindelöf, Plancherel and the sharp Nikolskii constant are known)

LeanOne-variable parts: TimeBand.harmonic_measure_ge (the harmonic measure of [−σ, σ] seen from the point iδ is (2/π) arctan(σ/δ)), transfer_of_ratio, poisson_exponent_lower and others.

There are two variants. Theorem T″ (termwise Cauchy–Schwarz) keeps the first power of u but moves the loss into the radius of convergence, and is 50–3000 times looser than the measured constant. Theorem T′ removes the price of shrinking the band, under the input (E1) "|Θ(f; σ′)| ≤ C1u‖f‖2 for |σ′| ≤ σ0". paper Measured, (E1) holds with σ0 = 2/L and C1 = 8, but there is no paper proof. computation

Measuring the transfer constant by its definition, maxf∈Vu tailδ(f)/‖f‖2 ≤ 3.4 e2L|δ| u holds independently of T, u and L. But the operator form without Vu, Mδ(I − Q)Mδ ≤ Ce2L|δ|(I − Q), is false. computation

L = 2, ε = 10−3. The main term is Sh(T*) − N(T*) = 53.72; the measured count is 53.

At L = 1 the main term is 6.51 and 𝔇 is 3–5, so the lower bound is positive but not of a meaningful size. This bound works better the larger L is — against the main term e2L, the error is O(L2). paper

① The slack is inside an e2L-dimensional Schur complement

WL = SL + QL cannot be treated as a perturbation: ‖QL‖ ≈ 4eL, while |λmin(SL)| grows only linearly in L. What can be written is a reduction by the Schur complement: on the complement with the k = n(L) sunk directions removed, P⊥WP⊥ > 0 holds (just barely). Weil's slack lies within n(L) ≈ e2L dimensions. A robust reduction needs k = N(T*), and then λmin(P⊥WP⊥) is nearly constant: 0.106 → 0.070 → 0.046. papercomputation

② The sunk eigenvectors are orthogonal to the space spanned by the zeros

With Z = span{v(γ) : γ ≤ T*} the space spanned by the zeros, the explicit formula gives in one line

The constant is O(1) because the zero vectors are nearly orthogonal (condition number at most 12.7). papercomputation Measured, it is deeper still, λj1.2–1.7, and the overlap for the directions that are not sunk matches the random-direction value N/m (negative control). computation This is a quantitative, finite-window version of the known observation that the radical of the Weil form contains the image of Connes–Consani's map E. known

③ The negative directions of SL, with the primes removed, are the low-frequency band of the Archimedean place

SL (pole + Archimedean) is positive definite for L < L0 = 0.41013 and indefinite beyond. Positivity continues past the classical positivity window (log 2)/2 = 0.34657. computation What the negative directions are:

• The Archimedean density Re ψ(1/4 + ir/2) − log π is −5.37218 at r = 0 and ≈ log(r/2) > 0 for large r. Its only positive root is r0 = 6.289835988836902779665 (not 2π; the difference is 0.106%). computation
• n−(SL) = n−(Archimedean only) − 1 holds in all 19 cells L = 0.30–3.00, exactly, for m = 48, 96, 192. n−(Archimedean only) grows with density r0/π = 2.00212. computation
• The pole term 2aaT, of rank 1 and positive semidefinite, removes exactly one negative direction.
• The negative directions of SL are also nearly orthogonal to the space of zeros (at L = 2, ‖ΠZv‖2 = 0.0022–0.0030, against 0.4171 for random directions). The reason takes one line: the negative band is r < r0, and the first zero γ1 = 14.1347 lies outside it. computation

The integral Ψ(r) of the Archimedean density is twice the Riemann–Siegel θ; r0 is the minimum point of θ, and the points where Ψ ≡ 0 (mod 2π) are the Gram points. known The two routes agreed to 40 digits. computation

④ Correspondence with the case of curves, and where it is missing

On the curve side, positivity closes just by "choosing one ample class and dropping to its orthogonal complement". On the ring-of-integers side, 2aaT does exactly one class's worth of work, but the Archimedean term creates L r0/π ≈ 2.002L negative directions, so one is not enough. known(left column) computation(the counts in the right column)

The linear algebra of the curve case was closed in Lean. For a symmetric bilinear form on a real vector space:

• LeanHodgeIndex.reverse_cauchy_schwarz — if Q h > 0 and Q y ≤ 0 for every y orthogonal to h, then Q x · Q h ≤ (B x h)2
• LeanHodgeIndex.castelnuovo_severi — if Q ≤ 0 on the orthogonal complement of the hyperbolic plane f1, f2, then Q D ≤ 2(B D f1)(B D f2)
• LeanHodgeIndex.no_ample_of_two_negatives — if B u v = 0, Q u < 0 and Q v < 0, then the kernel of any linear functional contains a w with Q w < 0

By the third, for L > 1.08, where n−(SL) ≥ 2, SL does not become positive semidefinite on any subspace of codimension 1 — an argument of the "one ample class" type cannot be used. But n−(SL) ≥ 2 itself is a numerical input. computation

⑤ An argument that splits off the low-frequency band is also ruled out in finite dimensions

Compress WL by the Slepian projection onto the band [0, r0), and the smallest eigenvalue is positive but only e4.91 − 17.44L (a fit to 13 points). In the low band, the Archimedean term and the prime term are each negative taken separately (−4.09 and −21.2 at L = 3), and positivity is what remains after two O(10) quantities cancel down to 10−20. Adding the prime powers in increasing order, the sign changes at the very end of the window. computation

• LeanBandSplit.cross_bound_of_nonneg (if positive semidefinite, then (B u w)2 ≤ Q u · Q w), two_block_nonneg (a sufficient condition for the band-splitting argument), band_split_counterexample (Q u = ε > 0 and Q w = 0 alone are not enough, and the violation is 1/ε deep)

Together with no_ample_of_two_negatives, both the "one ample class" type (impossible for L > 1.08) and the "split by band" type (impossible without knowing the cross block to an accuracy of e−8.7L) are ruled out at the level of finite-dimensional linear algebra. WL ⪰ 0 itself remains unproved. Lean(linear algebra) computation(the numerical inputs)

⑥ n(L) is "slack", not "crowding"

Suppose there are M teeth and nj zeros fall in tooth j. Put N = Σnj, crowding r = Σ(nj − 1)+, and empty teeth e = #{nj = 0}; then the identity

holds. Taking the teeth to be the Nyquist degrees of freedom (one per π/L) and counting up to T*, M = ⌊LT*/π⌋ and N = N(T*), and the difference between M − N and e2L − 7/8 is −1.24 to −0.14 in all 11 cells (L = 3: 402 against 402.554). computation So n(L) is the slack term M − N of this identity. The crowding r(L), on the other hand, has r/N(T*) → 0.16938 (the limit of the GUE single-gap formula), changes by only 4% when the gaps between zeros are rearranged, and carries no arithmetic content — the opposite of §05 ②, where rearranging Λ broke positivity. computation

• LeanPsiComb.crowded_add_card (the identity), excess_not_determine_crowded (with M = 3, N = 2, two configurations with crowding 0 and 1 — the slack does not determine the crowding) and others

⑦ Control: the "captured zeros" of the pseudo-Laplacian are a different kind of finiteness

The zeros captured as eigenvalues by the Bombieri–Garrett pseudo-Laplacian come with no guarantee of existence, and under the Riemann hypothesis and pair correlation they are at most 94%. known From interlacing (at most one eigenvalue between adjacent teeth), the upper bound on the number captured becomes a packing of intervalspaper, and putting in the actual zeros gives an unconditional, finite-height upper bound: at T = 1000, 613 of the 649 zeros of ζ (0.9445). The controls are Poisson 0.7025 and GUE 0.9315. computation The packing upper bound ⌊(B − A)/d⌋ + 1 and its sharpness are LeanPsiPacking.packing_card_le, packing_sharp. Where n(L) is a lower bound at "the crossing where capacity is overtaken by demand", this is an upper bound on the fraction "where capacity slightly exceeds demand but packing loses some", and it holds even if the discrete spectrum is empty, and even if the Riemann hypothesis is false.

The existence of sunk eigenvalues and the main term e2L of their number are known (Connes–Consani, arXiv:2106.01715 §2.5, §3; checked by reading the text). known Their L is the length of the support and the L of this article is the half-width, so the conversion is LCC = 2L, λ = eL, µ = λ2 = e2L.

Calibration. At LCC = log 2 they give the smallest eigenvalue of the even matrix of the archimedean contribution as ∼ 0.00133. Computing this article's SL in the even cosine basis gives 0.001449 / 0.001353 / 0.001335 / 0.001331 at m = 8/16/32/64, agreeing to three digits. This confirms at once the conversion, the fact that their archimedean contribution includes the pole term, and the normalisation of the basis. computation

A check at one external point. Against their −ln λmin = 109.65 at µ = 11 (L = 1.19895, T* = 69.115, N(T*) = 16), the decay law −ln λmin ≈ C·N(T*)/ln N(T*) gives 116.17 with C = 20.13 and 113.91 with C = 2π2. The ratios are 1.059 and 1.039, in the right direction (their value is for a restriction to a finite matrix, so it is larger than the true value). computation

The sunk eigenvectors are exactly their E(φn)

Measuring principal angles at L = 2 (µ = 54.598, 53 measured), 50 have cos θ equal to 1 to five decimal places, and 52 have > 0.99. Compressing WL to their 54 dimensions (φ2n = ψ2nψ0(0) − ψ0ψ2n(0), n = 1..54, ψm the prolate functions) gives eigenvalues from −4.7×10−14 to 0.27, 50 of them < 10−3. With 54 random dimensions, 0 have cos θ > 0.99 and the smallest eigenvalue of the compression is +1.38; with the fake weights from rearranging Λ(k), the smallest eigenvalue on the same 54 dimensions is −7 — this subspace sees arithmetic. By min–max, this compression is an explicit witness giving n(WL; 10−3) ≥ 50 without diagonalising WL. computation

But using their formula (3.4) as it stands drops this to 12. The basis for (3.4) is the sentence “act as if E(φn) would fulfill the equality E(φn)(u−1) = (−1)nE(φn)(u)” (arXiv:2106.01715 §3).

Measured at µ = 54.6, the odd component of E(φn) is 23–61% of the norm (median 48%), and this approximation does not hold. Even so, taking the even component, the conclusion survives — what is broken is not the conclusion but the route. computation Theorem T (§07 ③) is a statement bounding the leakage of elements of the sunk subspace after a complex translation by a power of the sinking u, and it belongs to the same family as the quantities that measure the violation of u → u−1 (t → −t). Their construction gives an explicit witness; Theorem T gives a bound on the side that has no witness. An inequality that actually bounds this violation by tailδ has not yet been written. paper(as positioning)

The lower bound on the sunk count is independent of the Riemann hypothesis, and can be used neither to prove nor to disprove the Riemann hypothesis.

• Only counts are used. n(L) = Sh(T*) − N(T*) is nothing but the integral of the difference between "the density L/π of degrees of freedom the window can hold" and "the density log(T/2π)/2π of zeros that must be cancelled", and never uses whether the zeros lie on the critical line. What it uses is the count N(T), which comes from the unconditional Riemann–von Mangoldt formula. The only place where information about the Riemann hypothesis enters is the eL in the transfer constant κ, and that is small against the main term e2L. So whether the lower bound holds or not, nothing comes back about where the zeros are.
• The slack is a vanishing quantity, living in a narrow place. The slack in Weil positivity is λ1(WL) ≈ e−2π2N(T*)/ln N(T*) (e−607 at L = 2), and it lives inside the n(L) ≈ e2L-dimensional Schur complement. Outside the complement the eigenvalues of SL are O(1), so a shift of O(1) by QL does not reach 0; only this bundle sinks. What supports the sign there is only the arithmetic of which log k each Λ sits on (rearrange it, and almost as many negative eigenvalues appear as there are sunk ones), and this framework has no arithmetic tool that bounds that sign from above.
• Neither perturbation, nor one ample class, nor splitting by band can be used (§09 ①④⑤).
• As long as the window is finite, only heights up to T* are visible. What is obtained is information about the zeros up to height 2πe2L, and the cost of L → ∞ grows exponentially, as e2L, in both dimension and prime powers.
• The same holds on the Connes–Consani side. The Weil positivity that implies the Riemann hypothesis is the semi-local version, and that is unproved (abstract of arXiv:2006.13771).

Zhu writes, for the same setting, that the positivity route alone does not reach the Riemann hypothesis. known This article does not overturn that judgement. All it adds is that, short of the point where the route fails to reach, the number of dimensions in which the slack lives gets a lower bound that does not assume the Riemann hypothesis.

Where the open items that have moved now stand is collected in What remains. Only what is open at present is listed here.

Known theorems used

Where we found no statement of the same shape in what we searched

These may be known. Even those whose proofs are complete are elementary, and we think it likely that specialists know them. In the Connes–Consani framework we found no statement of a theorem giving the lower bound, of the 1/k law with the combinatorial identity, or of the transfer inequality. None of them says anything about the Riemann hypothesis.

Open questions

Primary sources not yet obtained (in order of how much they bear on whether things are known): Li, X.-J., Prolate spheroidal wave functions, Sonine spaces, and the Riemann zeta function, J. Number Theory 2010 (not on arXiv) / Slepian's asymptotic expansions / Landau 1975, Landau–Widom 1980 / Weil 1952, Yoshida 1992.

What was closed in Lean 4 + mathlib is only finite-dimensional linear algebra, traces and counting, combinatorial identities, and one-variable integrals and inequalities. In all 12 files there are 0 sorry and no native_decide, and every one of the 73 lines of #print axioms output is a subset of propext, Classical.choice, Quot.sound (in fact all 73 lines are exactly these three).

The "Theorems" column is the number of theorems on which #print axioms was placed. TimeBand.binom_oddH_identity appears under the same name in TimeBandTrace2.lean (the individual version for k ≤ 12) and in TimeBandTrace3.lean (all k), and TimeBand.arctan_le_self in both Transfer files. Each file was checked on its own, and none imports another.

What it says, and what it does not. What is in Lean: the linear-algebra step (step (b)), finite-dimensional traces and counting, the geometric and algebraic core of tr A3, the combinatorial identity, φK with the Abel bound and the one-sided trace, the one-variable computations of the Poisson integral and termwise Cauchy–Schwarz, finite-dimensional Nikolskii/Bernstein, the maximum of the crossover, the linear algebra of the curve case and of band splitting, and the slack identity and packing. Theorem A, Theorem T, Theorem T′, Theorem C′, (E1), and the analysis of the 1/k law (the mean value of ψ, the integrals of the cluster amplitudes, Phragmén–Lindelöf, Plancherel, the infinite-dimensional version of min–max) are not in Lean. They are [paper]. The zeros of ζ, the explicit formula and WL itself are not in Lean either.

Sources and reproduction

What was searched: searches on the Weil form with cut support, numerics of the Weil quadratic form, prolates and Sonin spaces, the asymptotics of time–band limiting traces, and the pseudo-Laplacian, and the reference lists of the papers above. Lists of citing papers were not followed. On novelty, nothing stronger is said than "we found no statement of the same shape in what we searched". And, to repeat, no result on this page can be used either to prove or to disprove the Riemann hypothesis.