{"id":"palomar/PALOMAR-2026-08-22-000002","url":"https://github.com/mbaccaro-dev/mathematical-proofs/tree/f0ccae19f2cb5afdca00c42694d677c74dc492f6/MathematicalProofs/SelbergDivisorFeedback/Lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-22-000002-v1.json","repo":"https://github.com/mbaccaro-dev/mathematical-proofs","tags":["math.NT","msc:11N05","msc:11M26","analytic-number-theory","selberg-sieve","lean-formalization","von-mangoldt"],"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 sequence-level conditioning construction for Selberg divisor feedback. Two explicit perturbations of the von Mangoldt weight stay in the positive prime-power cone, approximate the divisor data to an arbitrary tolerance through twice the observation scale, separate their summatory outputs at a near-linear power scale, and retain one uniform linear Selberg bound.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-22","reactions":{},"formalized":true,"formalizes":[{"title":"Selberg Feedback and Approximate Divisor Data Do Not Stably Determine Square-Root Prime Error","identifier":"10.5281/zenodo.22005767","relationship":"formalizes"}]}