Smith normal form of the n-cycle class sum

Let Mn be the integer matrix of multiplication by the sum of all n-cycles on the center of ℤSn, in the conjugacy-class-sum basis. We determine its Smith normal form for every positive integer n. It has p(n) − n zero entries and nonzero invariant factors d0 = 1 and dr = ar r!/gcd(n, r) for 1 ≤ r < n, where ar = 2 when r ≡ n (mod 2) and ar = 1 otherwise, and p(n) is the partition number. This confirms Stanley's two conjectures for odd primes and twice odd primes, posed in 2019, when he also suggested that further data might lead to a conjecture for all n. Starting from the classical hook-character expression for the structure constants, we determine two integral coefficient lattices and reduce the induced pairing to an anti-triangular matrix with rowwise divisibility. The image-lattice theorem and the divisor chain are formalized in Lean from group-ring definitions, including a proof of the character expression. The equivalent diagonal form and the prime cases follow by the written basis-change and specialization arguments. Checked in Lean from the definitions; not yet reviewed by experts. Produced by AI models under the author's direction.