The cycle-sum identity (assembly)

The fixed-colouring sum of a permutation is its completed cycle-type product in the power sums of the colours; summed over the symmetric group this yields n! · h_n.

theorem RS.sum_fixedFun_eq_cycleProd {n N : ℕ} (x : Fin N → ℂ) (π : Equiv.Perm (Fin n)) : ∑ f : { f : Fin n → Fin N // f ∘ ⇑π = f }, ∏ i : Fin n, x (↑f i) = cycleProd (pVal x) π

The fixed-colouring sum of a permutation is its completed cycle-type product.

theorem RS.cycleSum_spec {n N : ℕ} (x : Fin N → ℂ) : ∑ π : Equiv.Perm (Fin n), cycleProd (pVal x) π = ↑n.factorial * hVal x n

The cycle sum at a realized specialization.

theorem RS.cycleSum_eq (t : ℕ → ℂ) (n : ℕ) : ∑ π : Equiv.Perm (Fin n), cycleProd t π = ↑n.factorial * newtonH t n

The cycle-sum identity: over any prospective power-sum sequence, the completed cycle-type products of all permutations sum to n! · h_n.