Open Research Index

Vulkin-prog/paper-c-lean

Brice Pouly

Palomar Registrypalomar/PALOMAR-2026-08-27-000008Aug 27, 2026math.NTscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-27-000008
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000008/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000008/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'