{"id":"palomar/PALOMAR-2026-08-27-000001","url":"https://github.com/BrandonMYates/tempered-xi-comparator/tree/d226851cc05dee3cad2244ce2660ad72b898a636","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000001-v1.json","repo":"https://github.com/BrandonMYates/tempered-xi-comparator","tags":["math.NT","math.CV","math.CA","msc:30D15","msc:30D10","msc:11M06","msc:44A15","riemann-zeta","complex-analysis","lean"],"score":0,"title":"BrandonMYates/tempered-xi-comparator","trust":"high","domain":"math.NT","source":"palomar","authors":["Brandon Yates"],"reviews":0,"subject":"math.NT","summary":"This project formalizes in Lean 4 the zero geometry of the odd channel of Riemann's kernel, refuting conjectures of X.-J. Yang (Fractals 32 (2024) 2340116). Let Phi be the kernel of Riemann's integral representation, Phi(u) = sum_{n>=1} (4 pi^2 n^4 e^{9u/2} - 6 pi n^2 e^{5u/2}) e^{-pi n^2 e^{2u}}, the positive even function whose cosh transform is the completed zeta function, and let F(w) = 2 int_0^infty Phi(u) sinh(wu) du be the odd channel of the same kernel; this is Yang's \"tempered xi function\", in shifted coordinates. Six statements are compared: F is entire; F has infinitely many…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"The zeros of the tempered xi function","identifier":"","relationship":"formalizes"}]}