A Lean 4 formalization of the results in "Low moments of the cycle count in products of conjugacy classes via content polynomials." The project builds on Mathlib and verifies the core theorems: a moment truncation principle showing that the $M$-th falling factorial moment of the cycle count $\mathrm{cyc}(\sigma\tau)$ depends only on partitions with at most $M$ subdiagonal boxes, a sparse mean formula restricting contributions to hook-like shapes $(a,b,1^k)$, explicit harmonic-number formulas for the first three moments in the $(n)\times(k^{n/k})$ model, algebraic identities for the variance and third central moment, and a distributional contraction reducing the $(n{-}1,1)\times(2^{n/2})$ model to the matching case on $n-2$ points.

The formalization contains 109 proved results across eight files with zero sorry and zero axiom declarations. Key constructions include Young diagrams with content polynomials defined as foldl products over box coordinates, elementary symmetric polynomials with a vanishing theorem proved by counting nonzero entries, the contraction theorem established via a cycle-count bound and an explicit disjoint-transposition witness, and the partition classification proved by showing a third row of width $\geq 2$ forces two content $-1$ boxes. Small-case correctness is additionally verified by native_decide for hook partitions, content polynomials, and elementary symmetric polynomial evaluations at concrete values.