Full permutation multiplicities

Abstract

The multiplicity factor of a full permutation partition includes its fixed-point factorial.

Definition 1.1 (The multiplicity factor).

$$\forall m\in \mathrm{Multiset}\left(\mathbb{N}\right),z\left(m\right)=\prod _{l\in \mathrm{toFinset}\left(m\right)}{l}^{\mathrm{count}\left(m,l\right)}\cdot \mathrm{factorial}\left(\mathrm{count}\left(m,l\right)\right)$$

Formalization. D5/S0/Asymptotics/WeightedProbability/PermutationMultiplicity.z (✓ std3).

Citation. The Tau Ceti contributors (2026). Conjugacy class sizes in the symmetric group. URL: https://github.com/TauCetiProject/TauCeti/blob/d7ac608e0c97f71e9e0dc210d26a470d974368d7/TauCeti/RepresentationTheory/Symmetric/ClassSize.lean.

Commentary.

For a multiset m of natural numbers, z(m) is the product of l^(count_m(l)) times count_m(l)! over its distinct entries. This is the Tau Ceti full-partition normalization used in the distinct-cycle-size limit.

Theorem 1.2 (Extending the finite product).

$$\forall m\in \mathrm{Multiset}\left(\mathbb{N}\right),\forall s\in \mathrm{Finset}\left(\mathbb{N}\right),\mathrm{Subset}\left(\mathrm{toFinset}\left(m\right),s\right)\Rightarrow z\left(m\right)=\prod _{l\in s}{l}^{\mathrm{count}\left(m,l\right)}\cdot \mathrm{factorial}\left(\mathrm{count}\left(m,l\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/WeightedProbability/PermutationMultiplicity.hz_prod (✓ std3). ∎

Citation. The Tau Ceti contributors (2026). Conjugacy class sizes in the symmetric group. URL: https://github.com/TauCetiProject/TauCeti/blob/d7ac608e0c97f71e9e0dc210d26a470d974368d7/TauCeti/RepresentationTheory/Symmetric/ClassSize.lean.

Commentary.

Any finite set containing the support gives the same product: missing entries have multiplicity zero and factor one.

Theorem 1.3 (Cycle type and fixed points).

$$\forall A\in Type,\mathrm{Fintype}\left(A\right)\Rightarrow \left(\mathrm{DecidableEq}\left(A\right)\Rightarrow \left(\forall sigma\in \mathrm{Perm}\left(A\right),z\left(\mathrm{parts}\left(\mathrm{partition}\left(sigma\right)\right)\right)=\mathrm{factorial}\left(\mathrm{tsub}\left(\mathrm{FintypeCard}\left(A\right),\mathrm{sum}\left(\mathrm{cycleType}\left(sigma\right)\right)\right)\right)\cdot \mathrm{prod}\left(\mathrm{cycleType}\left(sigma\right)\right)\cdot \mathrm{MultiplicityFactorialProduct}\left(\mathrm{cycleType}\left(sigma\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/WeightedProbability/PermutationMultiplicity.hz_perm (✓ std3). ∎

Citation. The Tau Ceti contributors (2026). Conjugacy class sizes in the symmetric group. URL: https://github.com/TauCetiProject/TauCeti/blob/d7ac608e0c97f71e9e0dc210d26a470d974368d7/TauCeti/RepresentationTheory/Symmetric/ClassSize.lean.

Commentary.

For every permutation of a finite carrier A, z(partition(sigma)) equals (card(A)-sum(cycleType(sigma)))! times prod(cycleType(sigma)) times the product of count(l)! over the distinct nontrivial cycle lengths. The omitted singleton cycles are restored by the first factorial. This normalization is adapted from Tau Ceti’s symmetric-group partition and class-size development; the complete Apache 2.0 license is retained in the cited note.

References

• Truth anchor: D5/S0/Asymptotics/WeightedProbability/PermutationMultiplicity.hz_perm
• Truth anchor: D5/S0/Asymptotics/WeightedProbability/PermutationMultiplicity.hz_prod
• Truth anchor: D5/S0/Asymptotics/WeightedProbability/PermutationMultiplicity.z