A Lean 4 formalization of "Poisson-cluster sumsets and sparse invariant-set sizes in wreath products." For a finite permutation group Γ ≤ S_k and a uniformly random element σ_n of the wreath product Γ ≀ S_n, this project formalizes the wreath action on kn points, the monodromy decomposition of induced cycles, multiplier sets arising from subset sums of cycle lengths, total-variation contraction under Markov kernels (the data-processing inequality), harmonic-number bounds (log t ≤ H_t ≤ 2 log t), and a saddlepoint framework including the existence and positivity of the group-dependent exponent δ_Γ. The main theorems give upper and lower bounds of order t^{−δ_Γ} (log t)^{−3/2} for the Poisson-cluster membership probability p_Γ(t), conditional on analytic inputs (local-to-global, dyadic smoothing, saddlepoint estimates) that are stated as explicit hypotheses, and prove intersection-emptiness with positive probability for r independent copies when rδ_Γ > 1 via p-series convergence.

The formalization contains zero sorry statements and zero axiom abuses. It builds on Lean 4.28.0 with Mathlib. Run lake build to verify.