{"id":"palomar/PALOMAR-2026-08-22-000004","url":"https://github.com/mbaccaro-dev/mathematical-proofs/tree/f0ccae19f2cb5afdca00c42694d677c74dc492f6/MathematicalProofs/SubpowerDyadicEnergy/Lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-22-000004-v1.json","repo":"https://github.com/mbaccaro-dev/mathematical-proofs","tags":["math.NT","msc:11M26","msc:11N37","analytic-number-theory","mobius-function","lean-formalization","squarefree-numbers"],"score":0,"title":"mbaccaro-dev/mathematical-proofs","trust":"high","domain":"math.NT","source":"palomar","authors":["Mayk Loide Baccaro"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 proof of the global power-of-two balance connecting dyadic defect, block variation, and positive Möbius-logarithm prefix energy. Eventual nonnegativity on exactly those dyadic blocks gives an explicit all-endpoint cubic energy bound. With the stated weighted-squarefree remainder estimate, the formalization also recovers the sharp 6/pi^2 leading coefficient and retains the complete finite-prefix correction.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-22","reactions":{},"formalized":true,"formalizes":[{"title":"Subpower Energy and Dyadic Defect Criteria for the Riemann Hypothesis","identifier":"10.5281/zenodo.22038521","relationship":"formalizes"}]}