{"id":"palomar/PALOMAR-2026-09-12-000003","url":"https://github.com/rwst/Confinement-Certificates/tree/e773310aa60d010038c3b1a02ee09dcaacce064d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-12-000003-v1.json","repo":"https://github.com/rwst/Confinement-Certificates","tags":["math.NT","math.DS","msc:11J71","msc:11K06","msc:37E05","number-theory","lean","dynamical-systems"],"score":0,"title":"Confinement schemas and the reach of block certificates for powers of rational numbers modulo one","trust":"high","domain":"math.NT","source":"palomar","authors":["Ralf Stephan"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 / Mathlib development of the second paper on the sets Z_{p/q}(s, s+t) = {ξ > 0 : {ξ(p/q)ⁿ} ∈ [s, s+t) for all n ≥ 0}, the generalized Z-numbers of Flatto, Lagarias and Pollington. The first paper built a corpus of block certificates for individual statements Z_{p/q}(U) = ∅. This paper replaces parts of that corpus by theorems, and then asks what the certificate format can and cannot reach. Thirty certificates in the regime p > q² collapse into one closed-form criterion on the single real parameter ε = {(p−q)s}, settling a set of positions of measure 1 − 2q²/(p(p+q)) at every base…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-12","reactions":{},"formalized":true,"formalizes":[{"title":"Confinement schemas and the reach of block certificates for powers of rational numbers modulo one","identifier":"","relationship":"formalizes"}]}