Add q-TSPP theorem statement

[tchow12000-coder]

This is a statement-only formalization of the q-TSPP theorem, together with its problem manifest.

We represent a plane partition as a (finite) order ideal (a.k.a. lower set) of 3-tuples of natural numbers. A plane partition is totally symmetric if it is invariant under the natural action of S₃; that is, if (i,j,k) is in the plane partition, then all permutations of the coordinates are also in the plane partition. In the generating polynomial, the exponent of q is the number of orbits, which is the same as the number of (i,j,k) with i ≤ j ≤ k.

The usual statement of the q-TSPP theorem expresses the generating polynomial as a rational function; here, to avoid any possible issues with dividing by zero, we multiply both sides by the denominator of the rational function to express the q-TSPP theorem as a polynomial identity. In Lean, it is natural to index the coordinates i, j, k starting from 0, so some care is needed to state the result correctly, since the Kauers-Koutschan-Zeilberger paper indexes i, j, k starting from 1.

The theorem statement is not difficult, but I am relatively new to Lean, so it would be nice if someone could manually confirm that the theorem statement is correct.

Testing

The following commands completed successfully, with the only warning being the use of 'sorry':

lake build LeanEval.Combinatorics.QTSPP
lake exe lean-eval validate-manifest --structure-only
lake exe lean-eval check-problem-build --module LeanEval.Combinatorics.QTSPP
lake exe lean-eval generate --problem q_tspp
lake exe lean-eval check-generated-builds --problem q_tspp