Content-grouped counting identity

The identity ∑ f, (∏ j, (fibreCard f j)!) · ∏ i, x (f i) = n! · hVal x n groups the sum over colourings f : Fin n → Fin N by content multiset and uses an orbit-stabilizer argument. The stabiliser count enters as a hypothesis, discharged as card_fixing_perms in StabCount.lean.

Basic helpers

theorem RS.prod_eq_content_prod {n N : ℕ} (f : Fin n → Fin N) (x : Fin N → ℂ) : ∏ i : Fin n, x (f i) = (Multiset.map x ↑(content f)).prod

The weight of a colouring depends only on its content.

theorem RS.fibreFactorial_eq_count_factorial {n N : ℕ} (f : Fin n → Fin N) : ∏ j : Fin N, (fibreCard f j).factorial = ∏ j : Fin N, (Multiset.count j ↑(content f)).factorial

The fibre-factorial product equals the count-factorial product.

theorem RS.content_comp_perm {n N : ℕ} (f : Fin n → Fin N) (σ : Equiv.Perm (Fin n)) : content (f ∘ ⇑σ) = content f

Precomposing by a permutation preserves content.

Transitivity of the content-class action

theorem RS.content_eq_exists_perm {n N : ℕ} (f g : Fin n → Fin N) (h : content f = content g) : ∃ (σ : Equiv.Perm (Fin n)), f ∘ ⇑σ = g

If two colourings have the same content, some permutation maps one to the other.

Existence of colourings with prescribed content

theorem RS.exists_content_eq {n N : ℕ} (s : Sym (Fin N) n) : ∃ (f : Fin n → Fin N), content f = s

Every s : Sym (Fin N) n is the content of some colouring.

Coset counting

The orbit-stabilizer identity

theorem RS.orbit_stab {n N : ℕ} (f₀ : Fin n → Fin N) (hstab₀ : {σ : Equiv.Perm (Fin n) | f₀ ∘ ⇑σ = f₀}.card = ∏ j : Fin N, (fibreCard f₀ j).factorial) : Fintype.card { g : Fin n → Fin N // content g = content f₀ } * ∏ j : Fin N, (Multiset.count j ↑(content f₀)).factorial = n.factorial

Orbit-stabilizer: class size times stabilizer size equals n!.

Main theorem

theorem RS.sum_fibreFactorial_weight' {n N : ℕ} (x : Fin N → ℂ) (hstab : ∀ (f : Fin n → Fin N), {π : Equiv.Perm (Fin n) | f ∘ ⇑π = f}.card = ∏ j : Fin N, (fibreCard f j).factorial) : ∑ f : Fin n → Fin N, ↑(∏ j : Fin N, (fibreCard f j).factorial) * ∏ i : Fin n, x (f i) = ↑n.factorial * hVal x n

The content-grouped count: weighting each colouring by its stabiliser size and its colour product sums to the factorial times the complete homogeneous value.