{"id":"palomar/PALOMAR-2026-08-22-000005","url":"https://github.com/mbaccaro-dev/mathematical-proofs/tree/11d59ae23fb0fe3d8591a00069bec47a868ac93f/MathematicalProofs/MobiusResidualComplexity/Lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-22-000005-v1.json","repo":"https://github.com/mbaccaro-dev/mathematical-proofs","tags":["math.NT","msc:11N37","msc:11A25","number-theory","mobius-function","lean-formalization"],"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 a residual-or-unmatched barrier for local Möbius cancellation. At every sufficiently large fixed-band scale, either the permitted edge length reaches the retained-prime product or every member of an explicit squarefree prime-product family is unmatched. Chebyshev estimates give the exact binomial and factorial population bounds. The product scale also converts residual rank to its logarithmic threshold with the exact limiting constant.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-22","reactions":{},"formalized":true,"formalizes":[{"title":"Logarithmic Residual-Complexity Barriers for Local Möbius Cancellation","identifier":"10.5281/zenodo.22006119","relationship":"formalizes"}]}