Every real primitive Dirichlet L-function has de Bruijn–Newman constant at most 9/32: a kernel-checked proof in Lean 4
Let χ be a real primitive Dirichlet character of conductor N ≥ 3 and parity k ∈ {0,1}. Let Λ(s,χ) = (N/π)^{(s+k)/2} Γ((s+k)/2) L(s,χ) be its completed L-function, and let H^χ_t(z) = ∫_0^∞ e^{tu²} Φ_χ(u) cos(zu) du be the de Bruijn–Newman heat flow of Λ(·,χ), normalised so that H^χ_0(z) = (1/8) Λ(1/2 + iz/2, χ). We give a proof, checked by the Lean 4 kernel, that for every such χ and every t ≥ 9/32 all zeros of H^χ_t are real. Equivalently, the generalised de Bruijn–Newman constant satisfies Λ_χ ≤ 9/32. The mathematics is not new, and we say exactly whose it is. De Bruijn's strip-contraction…
Comments and reviews
No comments yet.
API
curl /api/v1/records/hexagon/2610.00714
curl -X POST /api/v1/records/hexagon/2610.00714/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/hexagon/2610.00714/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'