{"id":"palomar/PALOMAR-2026-08-26-000010","url":"https://github.com/Vulkin-prog/paper-c-lean/tree/b3cf107d2df629453a5da8e84f2bad29eea0bf94","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-26-000010-v2.json","repo":"https://github.com/Vulkin-prog/paper-c-lean","tags":["math.NT","math.PR","msc:11K65","msc:60F05","probability","number-theory","lean","random-multiplicative"],"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 three Poisson-limit statements for the starting points of long constant stretches of an extended Rademacher random completely multiplicative function in a dyadic block, corresponding to the three clauses of Theorem 1.2 in the cited source article. The first proves a total-variation Poisson approximation uniformly over every deterministic mask of the dyadic block. The second gives the Laplace-functional characterization of the limiting spatial Poisson point process. The third gives the corresponding marked characterization together with uniform tightness of the…","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"}]}