{"id":"palomar/PALOMAR-2026-08-20-000007","url":"https://github.com/Vulkin-prog/paper-c-lean/tree/7dd863ab60a3b2b3a99fa4efcfb6503de7511811","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-20-000007-v1.json","repo":"https://github.com/Vulkin-prog/paper-c-lean","tags":["math.NT","math.PR","msc:11K65","msc:60F05","probability","number-theory","lean-formalization","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 a quantitative Poisson approximation for the starting points of long constant stretches of an extended Rademacher random completely multiplicative function in a dyadic block. The compared theorem uses a finite prime-sign cylinder and proves, uniformly in the critical window |L - log_2 N| <= C, that the total-variation distance to Pois(N/2^L) is O_C((log log N)^-2). It is conditional on three fully stated ordinary propositions specialized from Arratia--Goldstein--Gordon, Evertse--Silverman, and Nicolas--Robin; those propositions are theorem arguments, not Lean axioms.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-20","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"}]}