{"id":"palomar/PALOMAR-2026-09-25-000011","url":"https://github.com/jenkins-byu/nonnegativity-cutoffs-lean/tree/b3217f0e8367a677426daa461f8f79953532d80c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000011-v1.json","repo":"https://github.com/jenkins-byu/nonnegativity-cutoffs-lean","tags":["math.NT","msc:11F11","msc:11F30","modular-forms","sturm-bound","lean-formalization"],"score":0,"title":"Nonnegativity cutoffs for level-one modular forms","trust":"high","domain":"math.NT","source":"palomar","authors":["Paul Jenkins"],"reviews":0,"subject":"math.NT","summary":"A Lean formalization of the qualitative well-definedness of the nonnegativity Sturm bound A(k) for real level-one modular forms. For every weight k at least 12 and divisible by four, the formalization proves that a finite initial segment detects coefficientwise nonnegativity and that its optimal endpoint is attained as the greatest possible first negative Fourier-coefficient index.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true,"formalizes":[{"title":"Modular Forms with Only Nonnegative Coefficients","identifier":"doi:10.1007/s40993-026-00744-z","relationship":"formalizes"}]}