{"id":"palomar/PALOMAR-2026-08-26-000012","url":"https://github.com/Vulkin-prog/paper-c-lean/tree/37133861e5f7b350b6dcf9f5d61645aa7ed38bec","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-26-000012-v1.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 the first two moments and variance of the number of long constant-stretch starts of an extended Rademacher random completely multiplicative function in a dyadic block, together with the quantitative exponential estimate for the separated homogeneous two-start sum. Uniformly in the critical window, Theorem 1.4 gives the first-moment rate, second falling-factorial-moment convergence, R_2(N,L)=o_C(N^2), and variance convergence; Corollary 11.3 gives the stronger bound R_2(N,L) 0. Both compared statements are conditional on exactly two fully stated ordinary propositions…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-26","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"}]}