Dependencies

We define functions that contract and expand the domain and codomain of colorings:

• contractCodomain: Given a coloring \(f : [n] \to [m + 1]\) and a proof that \(f\) does not map any element to \(m\), this function returns \(f\) with codomain contracted to \([m]\).

• expandCodomain: Given a coloring \(f : [n] \to [m]\), this function returns \(f\) with codomain expanded to \([m + 1]\).

• contractDomain: Given a coloring \(f : [n + 1] \to [m]\), this function returns \(f\) with domain contracted to \([n]\).

• expandDomain: Given a coloring \(f : [n] \to [m + 1]\), this function returns \(f\) with domain expanded to \([n + 1]\), where \(f(n) = m\).

Let \(n, i, c \in \mathbb {N}\), \(\pi \in S_n\) and \(v\) be some boolean array indexed by \([n]\).
The function computeNumCyclesOfPermAux takes \(\pi , v, c\) and a proof that \(i \leq n\). It iterates over \(j \in [i - 1, \dots , 0]\) and if \(v[j] = \bot \), it increments \(c\) by \(1\) and sets \(v\) to \(\top \) at all indices that are in the same cycle as \(j\) with the visitCycle function. Then it returns updated \(c\).
The function computeNumCyclesOfPerm takes \(\pi \) and returns its number of cycles. It uses computeNumCyclesOfPermAux with \(i = n, v = \text{constant }\bot \text{ array of length n}, c = 0\).

Given \(g \in G\), the set of cycles of \(g\) is defined as \(X / \sim _g\), where \(\sim _g\) is the equivalence relation of being in the same cycle of \(g\):

The number of cycles of \(g\) is: \(c(g) = |X / \sim _g|\).
The number of elements in \(G\) with exactly \(i\) cycles is: \(|\{ g \in G \mid c(g) = i\} |\).

The dihedral group \(D_{2n}\) acts on \(\mathbb {Z}_n\) with:

computed in \(\mathbb {Z}_n\).

Given a permutation \(\pi \in S_X\), the set of cycles of \(\pi \) is defined as \(X / \sim _\pi \), where \(\sim _\pi \) is the equivalence relation of being in the same cycle of \(\pi \):

The number of cycles of \(\pi \) is:

The number of distinct colorings is defined as \(|Y^X/G|\).

For \(n \geq 1\), the number of distinct colorings of a bracelet with \(n\) beads and \(m\) colors is given by:

For \(n = 0\), we define that there is a single coloring of a bracelet with \(0\) beads. This is defined separately since we do not have a group \(D_{2\cdot 0}\). This definition is inspired by the fact that \(Y^\emptyset \) contains exactly one function.

The number of distinct colorings of a cube with \(m\) colors is given by:

For \(n \geq 1\), the number of distinct colorings of a necklace with \(n\) beads and \(m\) colors is given by:

For \(n = 0\), we define that there is a single coloring of a necklace with \(0\) beads. This is defined separately since we do not have a finite group \(\mathbb {Z}_0\). This definition is inspired by the fact that \(Y^\emptyset \) contains exactly one function.

The number of distinct colorings of \(n\) unordered, indistinguishable objects with \(m\) colors is

The number of weak compositions of \(n\) into \(m\) parts is:

This is the number of ways to separate \(n\) objects into \(m\) ordered sets.

We define functions that contract and expand permutations:

• permContract: Contracts \(\pi \in S_{n + 1}\) by removing \(n\) from the domain and remapping \(\pi ^{-1}(n) \mapsto \pi (n)\), if \(\pi ^{-1}(n) \neq n\). The result is a permutation in \(S_n\) whose inverse can be constructed by using the same procedure on \(\pi ^{-1}\).

• permExpand: Expands a permutation \(\pi \in S_n\) by adding \(n\) to the domain and defining \(\pi (n) = n\). The result is a permutation in \(S_{n + 1}\), whose inverse can be constructed by using the same procedure on \(\pi ^{-1}\).

We define two fundamental rotations of the cube:

• \(r = (0\ 1\ 2\ 3)\): A rotation of the cube by \(\frac{\pi }{2}\) around the vertical axis passing through the centers of the top and bottom faces. The front face moves to the position of the right face.

• \(s = (1\ 4\ 3\ 5)\): A rotation of the cube by \(\frac{\pi }{2}\) around the horizontal axis passing through the centers of the front and back faces. The right face moves to the position of the top face.

The set of rotational symmetries of the cube is given by:

The reasoning is as follows:

• First, we apply \(s\) at most three times to set the position of face \(1\).

• Then, we move face \(0\) to any other position using appropriate rotations. To move \(0\) to one of the faces in \(\{ 0, 1, 2, 3\} \), we apply \(r\) the necessary number of times. To move \(0\) to \(4\) or \(5\), we first apply \(r\) once to move \(0\) to \(1\), then apply \(s\) either once or three times.

Since we can move \(0\) to any position and \(1\) to any position adjacent to the new position of \(0\) (by applying \(s\) an appropriate amount of times in the beginning), this results in \(6 \times 4 = 24\) distinct rotational symmetries. Because the entire cube configuration is determined by the new positions of faces \(0\) and \(1\), we have all rotational symmetries of the cube.

The Stirling numbers of the first kind count the number of permutations of a set of size \(n\) with exactly \(k\) cycles:

where \(c(\pi )\) denotes the number of cycles in the permutation \(\pi \).

Let \(n \in \mathbb {N}\), \(\pi \in S_n\), \(x, y \in [n]\) and \(v\) be a boolean array indexed by \([n]\).
The function visitCycleAux takes \(v\) and a proof of \(\exists m \in \mathbb {N}, \pi ^{m + 1}(x) = y\). It returns an array that is identical to \(v\) except that it is set to \(\top \) at all indices in \(\{ x, \pi (x), \pi ^2(x), \dots , \pi ^{-1}(y)\} \). The function works by recursively calling itself with \(v := (v[x] = \top ), x := \pi (x)\) until it reaches \(\pi (x) = y\), then it returns \(v[x] = \top \). The proof ensures termination by guaranteeing that \(\pi (x) = y\) will eventually hold.
The function visitCycle takes \(\pi , x, v\), and returns an array identical to \(v\) except that it is set to \(\top \) at all indices that are in the same cycle of \(\pi \) as \(x\). It uses visitCycleAux with \(y = x\) and a proof of \(\exists m, \pi ^{m + 1}(x) = x\) from Proposition 11.

The function computeNumCyclesOfPerm given \(\pi \) computes the number of cycles of \(\pi \).

The function computeNumCyclesOfPerm given \(\pi \) computes the cardinality of some set of representatives of cycles of \(\pi \) - that is a set that contains exactly one element from every cycle of \(\pi \).

Let \(\pi \in S_n\), \(v\) be a boolean array that is set to \(\top \) at exactly those indices that are in the same cycle of \(\pi \) as some element in \(\{ i, \dots , n - 1\} \) and \(c\) be the cardinality of some set \(S\) of representatives of those cycles of \(\pi \) that contain some element in \(\{ i, \dots , n - 1\} \).
Then computeNumCyclesOfPermAux given \(\pi , v, c\) returns the cardinality of some set of cycle representatives of \(\pi \).

The function computeNumDistinctColorings computes the number of distinct colorings of \(X\) with colors in \(Y\) under the group action of \(G\). It uses Pólya’s enumeration theorem and the function computeNumCyclesOfPerm to count cycles of permutations:

The number of distinct colorings of a bracelet can be computed using the computeNumDistinctColorings function.

The number of distinct colorings of a cube can be computed using the computeNumDistinctColorings function.

The number of distinct colorings of a necklace can be computed using the computeNumDistinctColorings function.

Let \([x]\) denote the equivalence class of \(x\) in \(X/\sim _g\).
Let \(\varphi : (Y^X)^g \to Y^{X/\sim _g}\) be defined by \(\varphi (f) = ([x] \mapsto f(x'))\), where \(x'\) is some element of \([x]\).
Let \(\varphi ^{-1} : Y^{X/\sim _g} \to (Y^X)^g\) be defined by \(\varphi ^{-1}(f) = (x \mapsto f([x]))\).
Then \(\varphi \) and \(\varphi ^{-1}\) are well-defined and mutually inverse. Therefore we have a bijection between \((Y^X)^g\) and \(Y^{X/\sim _g}\).

Let \(\pi \) be a permutation on a finite set \(X\), and \(x \in X\). Then there exists some \(n \in \mathbb {N}\) such that:

For any \(g \in G\):

Let \(\pi \) be a permutation such that \(\pi ^{n + 1}(x) = x\) for some \(n \in \mathbb {N}\). Then for any \(k \in \mathbb {Z}\) there exists an \(m \in [n + 1]\) such that:

For all \(x \in S\), we have:

Given a group action of \(G\) on \(X\), we can define an induced group action of \(G\) on \(Y^X\) by:

Given a group action of \(G\) on \(X\), we can define an induced group action of \(G\) on \([|X|]\) with:

For a permutation \(\pi \in S_X\) and a set \(S\) containing exactly one element from each cycle of \(\pi \), we have \(c(\pi ) = |S|\).

The number of distinct colorings of \(X\) with colors in \(Y\) under the group action of \(G\) on \(X\) is equal to the number of distinct colorings of \([|X|]\) with colors in \(Y\) under the induced group action of \(G\) on \([|X|]\).

(Pólya’s enumeration theorem) The number of distinct colorings of \(X\) with colors in \(Y\) under the group action of \(G\) on \(X\) is:

A version of the theorem that preserves the fact that \(\sum _{g \in G} |Y|^{c(g)}\) is divisible by \(|G|\) is also provided:

The number of distinct colorings of \(n\) unordered, indistinguishable objects with \(m\) colors is equal to the number of weak compositions of \(n\) with \(m\) parts.

A recurrence formula for the number of distinct colorings of \(n + 1\) unordered, indistinguishable objects with \(m + 1\) colors:

Let \(\pi \in S_n\) be such that \(\pi (i) = n\) for some \(i {\lt} n\). Then \(\pi (\pi (i)) {\lt} n\).

Let \(\pi \) be a permutation such that \(\pi ^n(x) = x\) for some \(n \in \mathbb {N}\). Then for any \(m, r \in \mathbb {N}\), we have:

Let \(M\) be a monoid. If \(m \in M\) satisfies \(m^n = 1\), then for any \(i, j \in [n]\), we have:

\(S\) is a subgroup of \(S_6\).

For all \(x \in S\) and \(n, m, k \in \mathbb {N}\), we have:

For any \(n, m \in \mathbb {N}\) with \(m {\gt} 0\), we have

Additionally:

• If \(n = m = 0\), the sum evaluates to \(1\) in Lean, since \(0^0 = 1\).

• If \(n {\gt} 0\) and \(m = 0\), the sum evaluates to \(0\).

The function visitCycle given \(\pi , x, v\) returns an array identical to \(v\), except that it is set to \(\top \) at all indices that are in the same cycle of \(\pi \) as \(x\).

The function visitCycleAux given \(v, (\exists m \in \mathbb {N}, \pi ^{m + 1}(x) = y)\) returns an array that is set to \(\top \) at all entries where \(v\) is set to \(\top \).

Let \(m \in \mathbb {N}\) be the smallest number satisfying \(\pi ^{m + 1}(x) = y\). Then visitCycleAux given \(v, (\exists k \in \mathbb {N}, \pi ^{k + 1}(x) = y)\) returns an array that:

• is identical to \(v\) at all indices not in the same cycle as \(x\),

• is set to \(\top \) at all indices in \(\{ x, \pi (x), \pi ^2(x), \dots , \pi ^m(x)\} \),

• has the same size as \(v\).