PF4

The kernel

Riemann's Ξ function, the completed zeta function on the critical line, is, up to a change of scale, the cosine transform of one positive, even, rapidly decaying function. In the normalization of the paper, which is twice de Bruijn's,

Φ(t) = Σ_n≥1 (4π²n⁴e^9t/2 − 6πn²e^5t/2) e^−πn²e2t, t ≥ 0,

extended to negative t by symmetry. Every term is positive because 2π is larger than 3. De Bruijn studied this kernel in 1950, Csordas and Varga drew moment inequalities from it, and it sits at the start of the de Bruijn–Newman line of work on the zeros of Ξ.

Pólya frequency order

Schoenberg called a function f Pólya frequency of order r when, for every k up to r and every pair of increasing node lists x₁ < … < x_k and y₁ < … < y_k, the determinant of the k-by-k matrix f(x_i − y_j) is nonnegative. Order one says f is nonnegative. Order two says log f is concave. Higher orders control sign changes: convolving with a function of order r never increases the number of sign changes of a signal that has fewer than r of them, which is why the property appears in smoothing, statistics and approximation. The order is strict when every such determinant is positive.

The theorem

For every k from 1 to 4 and every pair of strictly increasing real lists, det[Φ(x_i − y_j)] > 0. With h = 211/2000, the 5-by-5 determinant det[Φ((i − j)h)], i and j running from 0 to 4, is negative. The exact global order is therefore four.

The proof

Order four has to be shown for every pair of four-node lists at once, so no amount of sampling can settle it. The proof goes in four steps.

1. Two log-curvature quantities of Φ, called q and F₂, are positive on the whole line. That gives strict order three and the positivity of a three-point function Λ.
2. When all four nodes of a minor merge, what remains is a single function C₄ of one variable. It is positive everywhere. The proof treats the two leading theta terms exactly, with rational polynomial inequalities on fixed intervals and Taylor bounds, and controls all the remaining terms with geometric tail estimates.
3. Quotient and Wronskian identities reduce an arbitrary fourth-order minor to the sign of one derivative, ∂_ξΨ, of a three-point function Ψ.
4. In an increasing curvature coordinate, the numerator of that derivative becomes δΛ ∫ Δ(t) C₄(t) / (Q(t)⁶ κ(t)²) dt, where Δ is a cumulative gap between two explicit triangular weights. The gap is positive by exact mass identities and one algebraic sign change, so the derivative has a fixed sign, and the reduction turns that sign into strict positivity of every fourth-order minor.

That integral is where the method shows: wherever an earlier version of the argument rested on a numerical bound, the work kept going until an exact identity took its place.

Checking it

The final theorem is checked by the Lean 4 kernel against mathlib. Every finite sign enters as an exact integer or rational inequality, so no floating-point value discharges a step, and the axiom audit prints only Lean's three standard axioms, propext, Classical.choice and Quot.sound: nothing is left unproved or taken on trust. What remains for a reader to check is the statement itself, and it is short: the kernel is the paper's own, built from the literal theta sum, and Pólya frequency order is the textbook definition over every strictly increasing pair of real node lists.

cd proof/formal
lake build
lake env lean PF4/Audit.lean  # prints the axiom closure

Two Python programs in the repository replay the finite arithmetic printed in the paper. The paper, certificates, proof records and replay tools are archived under DOI 10.5281/zenodo.21487371, release pf4-paper-v2.1.0.

References

• I. J. Schoenberg, “On Pólya frequency functions. II. Variation-diminishing integral operators of the convolution type,” Acta Sci. Math. (Szeged) 12 (1950), 97–106.
• S. Karlin, Total Positivity, Vol. I, Stanford University Press, 1968.
• A. Belton, D. Guillot, A. Khare and M. Putinar, “Preservers of totally positive kernels and Pólya frequency functions,” Math. Res. Rep. 3 (2022), 35–56, arXiv:2110.08206.
• N. G. de Bruijn, “The roots of trigonometric integrals,” Duke Math. J. 17 (1950), 197–226, doi:10.1215/S0012-7094-50-01720-0.
• G. Csordas and R. S. Varga, “Moment inequalities and the Riemann Hypothesis,” Constr. Approx. 4 (1988), 175–198, doi:10.1007/BF02075457.
• K. Gröchenig, “Schoenberg's theory of totally positive functions and the Riemann zeta function,” arXiv:2007.12889.
• J. Rainstar, “The Riemann kernel is globally PF4,” revised 22 July 2026, PDF, doi:10.5281/zenodo.21487371.