{"id":"palomar/PALOMAR-2026-08-24-000002","url":"https://github.com/rwst/Confinement-Certificates/tree/eb810d8f86e49b2b8e058d02a9edac9e5fedafc8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-24-000002-v2.json","repo":"https://github.com/rwst/Confinement-Certificates","tags":["math.NT","math.DS","msc:11J71","msc:11K06","msc:37B10","dynamical-systems","z-numbers","lean-formalization"],"score":0,"title":"rwst/Confinement-Certificates","trust":"high","domain":"math.NT","source":"palomar","authors":["Ralf Stephan (direction, review, paper author)"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 / Mathlib development of a paper on the emptiness theory of 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, at and beyond the window length 1/p. The paper introduces block certificates --- finite integer witnesses, rechecked from scratch by the Lean proof kernel, whose soundness rests on the aperiodicity lemma alone --- and uses them to pass the length-$1/p$ line: $\\Zset_{3/2}(1/6,13/24)=\\emptyset$ (window length $3/8>1/3$), $\\Zset_{3/2}(961/3600,2427/3600)=\\emptyset$ (length $733/1800$), and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-06","reactions":{},"formalized":true,"formalizes":[{"title":"Confinement certificates for powers of rational numbers modulo one","identifier":"https://doi.org/10.13140/RG.2.2.36190.19520","relationship":"formalizes"}]}