{"id":"palomar/PALOMAR-2026-08-27-000008","url":"https://github.com/Vulkin-prog/paper-c-lean/tree/b3cf107d2df629453a5da8e84f2bad29eea0bf94","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000008-v2.json","repo":"https://github.com/Vulkin-prog/paper-c-lean","tags":["math.NT","math.PR","msc:11K65","msc:60F05","probability","number-theory","lean","multiplicative-functions"],"score":0,"title":"Vulkin-prog/paper-c-lean","trust":"high","domain":"math.NT","source":"palomar","authors":["Brice Pouly"],"reviews":0,"subject":"math.NT","summary":"Lean 4 formalization of global and finite-prefix Poisson laws for the starting points of long constant stretches of an extended Rademacher random completely multiplicative function, corresponding to Theorem 16.2 and Corollary 16.4 of the cited source article. The selected declarations give the global interior start-count law on a finite prime-sign cylinder, its recentering at M/2^L, the corresponding theorem on the infinite Rademacher product, and the finite-prefix start-count and longest-stretch law. All asymptotics are uniform in the critical window |L - log_2 M| <= C. Each declaration is…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"A critical Poisson law in a dyadic block -- Starting points of long constant stretches of an extended Rademacher random completely multiplicative function","identifier":"https://doi.org/10.33774/coe-2026-z3l74","relationship":"adapts"}]}