{"id":"palomar/PALOMAR-2026-08-29-000004","url":"https://github.com/yuhangshi888/zeta-simple-zeros-673316977/tree/7cfd0ce9a9ef1615889b5c1191fac5de41f13960/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000004-v1.json","repo":"https://github.com/yuhangshi888/zeta-simple-zeros-673316977","tags":["math.NT","msc:11M26","riemann-zeta","number-theory","lean-formalization","zeros"],"score":0,"title":"yuhangshi888/zeta-simple-zeros-673316977","trust":"high","domain":"math.NT","source":"palomar","authors":["Yuhang Shi"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 and Mathlib formalization of the supporting-plane and exact-arithmetic portion of the finite-dimensional argument in Yuhang Shi's research draft on simple zeros of the Riemann zeta function. It proves a conditional scalar two-certificate supporting-plane implication, its explicit piecewise-square-root specialization at block length 219, and the exact strict comparison above 673316977/10^9 for the resulting local assembly expression. The spectral derivation of the trace-envelope alternative, the upstream seven- and nine-point interval certificates, and the analytic passage from…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-29","reactions":{},"formalized":true,"formalizes":[{"title":"A two-certificate trace-energy deduction for simple zeros of the Riemann zeta function","identifier":"doi:10.5281/zenodo.21926962","relationship":"formalizes"}]}