{"id":"palomar/PALOMAR-2026-10-22-000040","url":"https://github.com/wcook04/plectis-erdos-lean/tree/d8db022f33199491ba88d47fac6d66f8690f2c1a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000040-v1.json","repo":"https://github.com/wcook04/plectis-erdos-lean","tags":["math.NT","msc:11J72","msc:11A05","irrationality","factorials","reciprocal-series","number-theory"],"score":0,"title":"Carry and divisor-channel criteria for the factorial-minus-one reciprocal series","trust":"high","domain":"math.NT","source":"palomar","authors":["Will Cook"],"reviews":0,"subject":"math.NT","summary":"For the reciprocal series with denominators n! - 1, the selected Lean theorems give an exact carry characterization of rationality, divisor-channel coordinates, and a finite gcd moment certificate. Companion-orbit and complementary tail criteria are included with their stated hypotheses. These structural results do not certify the paper's large computed denominator exclusions or resolve the irrationality question.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true}