2.2 Euler’s pentagonal number theorem and Jacobi’s triple product identity
2.2.1 Euler’s pentagonal number theorem
For any \(k\in \mathbb {Z}\), define a nonnegative integer \(w_{k}\in \mathbb {N}\) by
This is called the \(k\)-th pentagonal number.
We have
Set \(q=x^{3}\) and \(z=-x\) in Theorem 2.81. (This means that we apply Theorem 2.81 to \(a=3\) and \(b=1\) and \(u=1\) and \(v=-1\).) We get
The left hand side of this equality simplifies as follows:
since each positive integer \(k\) can be uniquely represented as \(3n-1\) or \(3n-2\) or \(3n\) for some positive integer \(n\).
Comparing this with (3), we obtain
(here, we have substituted \(k\) for \(-\ell \) in the sum, and used the identity \(3\ell ^{2}+\ell = 2w_{-\ell }\)).
Now, we “substitute \(x\) for \(x^{2}\)” in this equality using Lemma 2.119. As a result, we obtain
This is Euler’s pentagonal number theorem (Theorem 2.68).
The Lean proof proceeds by first proving the identity over \(\mathbb {Q}\) (using Lemma 2.122, Lemma 2.120, Lemma 2.121, and Lemma 2.119), and then transferring to \(\mathbb {Z}\) by comparing coefficients via the ring homomorphism \(\mathbb {Z}\to \mathbb {Q}\) (using Lemma 2.123).
Pentagonal number properties
The function \(k\mapsto w_k\) is injective: if \(w_j = w_k\) then \(j = k\).
By monotonicity on the positive integers (strictly increasing) and on the negative integers (also strictly increasing in absolute value), and the fact that \(w_k = w_j\) forces \(k, j\) to have the same sign.
For any \(n\in \mathbb {N}\), the set \(\{ k\in \mathbb {Z} : w_k {\lt} n\} \) is finite.
Since \(w_k\) grows quadratically (specifically \(w_k \geq |k|\) for \(k\neq 0\)), only finitely many \(k\) satisfy \(w_k {\lt} n\).
The pentagonal coefficient at \(n\in \mathbb {N}\) is
This is well-defined by the injectivity of pentagonal numbers (Lemma 2.69).
- AlgebraicCombinatorics.pentagonalCoeff n = match AlgebraicCombinatorics.pentagonalNumberInverse n with | some k => (-1) ^ k.natAbs | none => 0
For any \(k\in \mathbb {Z}\), \(\mathrm{pentagonalCoeff}(w_k) = (-1)^{|k|}\).
Immediate from the definitions, since the inverse lookup recovers \(k\) from \(w_k\) by injectivity (Lemma 2.69).
If \(m\in \mathbb {N}\) is not a pentagonal number (i.e., \(w_k \neq m\) for all \(k\in \mathbb {Z}\)), then \(\mathrm{pentagonalCoeff}(m) = 0\).
By definition of pentagonal coefficients.
Generating function definitions
The pentagonal series is the formal power series
The Euler product is the infinite product
defined as a multipliable product in the Pi topology on \(R[[x]]\).
- AlgebraicCombinatorics.eulerProduct = ∏' (k : ℕ), (1 - PowerSeries.X ^ (k + 1))
The partition generating function is
where \(p(n)\) denotes the number of partitions of \(n\).
The partition generating function satisfies
By Mathlib’s partition generating function infrastructure.
The Euler product times the partition generating function equals \(1\):
Each factor \((1-x^k)\) cancels with its inverse, using the per-term identity \((1 + x^k + x^{2k} + \cdots )(1 - x^k) = 1\) and multipliability of the products.
For each positive integer \(n\), we have
We have
(by Theorem 2.30) and
(by Theorem 2.68). Multiplying these two equalities, we obtain
Now, let us fix a positive integer \(n\). We shall compare the \(x^{n}\)-coefficients on both sides of (7).
The \(x^{n}\)-coefficient on the left hand side of (7) is
But the \(x^{n}\)-coefficient on the right hand side of (7) is \(0\) (since \(n\) is positive). Hence, comparing the coefficients yields
Solving this for \(p\left( n\right) \), we find
Corollary 2.79 is thus proved.
2.2.2 Jacobi’s triple product identity
The identity
In the ring \(\left( \mathbb {Z}\left[ z^{\pm }\right] \right) \left[ \left[ q\right] \right] \), we have
Let \(a\) and \(b\) be two integers such that \(a{\gt}0\) and \(a\geq \left\vert b\right\vert \). Let \(u,v\in \mathbb {Q}\) be rational numbers with \(v\neq 0\). In the ring \(\mathbb {Q}\left[\left[ x\right]\right] \), set \(q=ux^{a}\) and \(z=vx^{b}\). Then,
Borcherds’ state infrastructure
A level is a number of the form \(p+\frac{1}{2}\) with \(p\in \mathbb {Z}\). A state is a set of levels that contains all but finitely many negative levels, and only finitely many positive levels.
For any state \(S\), we define:
the energy of \(S\) to be
\[ \operatorname {energy}S:=\sum _{\substack{[p, {\gt}, 0, ;, \\ , p, \in , S]}}2p -\sum _{\substack{[p, {\lt}, 0, ;, \\ , p, \notin , S]}}2p \in \mathbb {N}; \]the particle number of \(S\) to be
\[ \operatorname {parnum}S:=\left(\text{\# of positive levels in } S\right) -\left(\text{\# of negative levels not in } S\right)\in \mathbb {Z}. \]
The set of levels in this state
Only finitely many nonnegative levels (p ≥ 0, representing positive half-integers p+1/2 > 0) are in the state
Only finitely many negative levels (p < 0, representing negative half-integers p+1/2 < 0) are NOT in the state
For \(\ell \in \mathbb {Z}\), the \(\ell \)-ground state is
For any \(\ell \in \mathbb {Z}\), we have \(\operatorname {energy}G_{\ell }=\ell ^{2}\) and \(\operatorname {parnum}G_{\ell }=\ell \).
If \(\ell \geq 0\), the energy is \(1+3+5+\cdots +(2\ell -1)=\ell ^{2}\) and the particle number is \(\ell -0=\ell \). If \(\ell {\lt}0\), the energy is \(-(-1)-(-3)-\cdots -(2\ell +1)=\ell ^{2}\) and the particle number is \(0-(-\ell )=\ell \).
If \(S\) is a state, \(p\in S\), and \(q\) is a positive integer such that \(p+q\notin S\), then the state
is said to be obtained from \(S\) by letting the electron at level \(p\) jump \(q\) steps to the right.
A jump by \(q\) steps keeps the particle number unchanged and raises the energy by \(2q\).
Three cases are checked: the particle jumps from a positive to a positive level, from a negative to a positive level, or from a negative to a negative level.
For any partition \(\lambda =(\lambda _{1},\lambda _{2},\ldots ,\lambda _{k})\) and any \(\ell \in \mathbb {Z}\), the excited state \(E_{\ell ,\lambda }\) is defined by starting with the \(\ell \)-ground state \(G_{\ell }\) and then successively letting the \(k\) electrons at the highest levels jump \(\lambda _{1},\lambda _{2},\ldots ,\lambda _{k}\) steps to the right, respectively:
The excited state \(E_{\ell ,\lambda }\) is reachable from the ground state \(G_\ell \) by a sequence of jumps (in the sense of Definition 2.85).
By induction on the number of parts: starting from \(G_\ell \), one performs \(k\) successive jumps of sizes \(\lambda _1, \ldots , \lambda _k\). The intermediate state construction ensures each jump is valid (source is occupied, target is vacant).
The excited state \(E_{\ell ,\lambda }\) has energy \(\ell ^{2}+2|\lambda |\) and particle number \(\ell \).
The state \(E_{\ell ,\lambda }\) is obtained from \(G_{\ell }\) by \(k\) jumps of \(\lambda _{1},\ldots ,\lambda _{k}\) steps. Each jump by \(q\) steps raises the energy by \(2q\) and keeps the particle number unchanged. Since the ground state has energy \(\ell ^{2}\) and particle number \(\ell \), the result follows.
The partition–state bijection
For fixed \(\ell \in \mathbb {Z}\), the map \(\lambda \mapsto E_{\ell ,\lambda }\) is injective: if \(E_{\ell ,\mu _1} = E_{\ell ,\mu _2}\), then \(\mu _1 = \mu _2\).
Two excited states are equal if and only if their level sets agree. The partition \(\lambda \) is recovered from the excited levels via \(\lambda _i = (\)
\(\)i\(-th largest excited level\)) - (ℓ- i + )\(\), so equal level sets force equal partitions. The key step is that \(i\mapsto \lambda _i - i\) is strictly decreasing for sorted parts, making the level encoding injective.
For any \(\ell \in \mathbb {Z}\) and any state \(S\) with \(\operatorname {parnum}(S) = \ell \), there exists a partition \(\mu \) such that \(S = E_{\ell ,\mu }\).
Given \(S\) with particle number \(\ell \), we construct \(\mu \) by listing the excited levels of \(S\) (those above the base level) in decreasing order and computing \(\mu _i = (\)
\(\)i\(-th excited level\)) - (ℓ- i + )\(\). The proof shows these differences are positive integers forming a valid partition, and that the resulting excited state equals \(S\).
For each \(\ell \in \mathbb {Z}\), the map
is a bijection.
The global map
is a bijection. The inverse sends a state \(S\) to \((\operatorname {parnum}(S), \mu )\) where \(\mu \) is the unique partition with \(E_{\operatorname {parnum}(S), \mu } = S\).
Injectivity: if \(E_{\ell _1,\mu _1} = E_{\ell _2,\mu _2}\), comparing particle numbers gives \(\ell _1 = \ell _2\), and then injectivity of \(\Phi _\ell \) gives \(\mu _1 = \mu _2\). Surjectivity: any state \(S\) has particle number \(\ell = \operatorname {parnum}(S)\), and by the surjectivity of \(\Phi _\ell \), there exists \(\mu \) with \(E_{\ell ,\mu } = S\).
For any state \(S\), there exists \(n\geq 0\) such that
In particular, the energy is always at least \(|\operatorname {parnum}(S)|^2\), and the excess is always even.
Finset pair bijection with states
Given a pair \((P, N)\) of finite subsets of \(\mathbb {N}\), define the state \(\operatorname {fromFinsetPair}(P, N)\) whose levels are
Here \(P\) encodes the nonneg levels present, and \(N\) encodes the negative levels missing (with \(n \in N\) meaning level \(-(n+1)\) is missing).
For any pair \((P, N)\) of finite subsets of \(\mathbb {N}\),
For nonneg level \(n\in P\): contribution is \(2n+1\). For missing negative level \(-(n+1)\) with \(n\in N\): \(|{-}(n{+}1)| = n+1\), so contribution is \(2(n+1)-1 = 2n+1\). Both give \(2n+1\).
For any pair \((P, N)\) of finite subsets of \(\mathbb {N}\),
The number of nonneg levels present is \(|P|\), and the number of negative levels missing is \(|N|\).
The map \((P,N)\mapsto \operatorname {fromFinsetPair}(P,N)\) is a bijection from pairs of finite subsets of \(\mathbb {N}\) to states.
Injectivity: \(P\) and \(N\) are recovered from any state \(S\) by taking \(P = \{ p \geq 0 : p \in S\} \) and \(N = \{ n \in \mathbb {N} : -(n+1) \notin S\} \). Surjectivity: any state \(S\) equals \(\operatorname {fromFinsetPair}(P, N)\) where \(P\) and \(N\) are constructed as above.
For any \(d\in \mathbb {N}\) and function \(f:\mathbb {Z}\to \mathbb {Z}[z^{\pm }]\),
Both sums are over finite sets, and equality holds because both sides can be rewritten as \(\sum _{S:\operatorname {energy}(S)=d} f(\operatorname {parnum}(S))\) using the two bijections (finset pairs and integer–partition pairs with states).
Jacobi ring definitions and state generating function
The state monomial with energy \(e\) and particle number \(p\) is the element \(q^e z^p \in (\mathbb {Z}[z^{\pm }])[[q]]\).
The state generating function is the formal sum over all integer–partition pairs \((\ell , \mu )\):
It is defined as the formal sum \(\sum '_{(\ell , \mu )} q^{\ell ^2 + 2|\mu |} z^\ell \) over all integer–partition pairs.
The partition generating function in JacobiRing is
- AlgebraicCombinatorics.partitionGenFunJacobi = ∑' (p : (n : ℕ) × n.Partition), PowerSeries.X ^ (2 * p.fst)
The \(z\)-dependent product is
The \(q\)-only product is
LHS factorization and product–state connection
The LHS of Jacobi’s identity factors as
Each factor in the LHS product is \((1+q^{2n-1}z)(1+q^{2n-1}z^{-1})(1-q^{2n})\), which splits into the product of the first two factors (which form the \(z\)-dependent product) and the third factor (which forms the \(q\)-only product). The infinite product distributes because both sub-products are multipliable.
The partition generating function times the \(q\)-only product equals \(1\):
Per-term cancellation: \((1 + q^{2k} + q^{4k} + \cdots )(1 - q^{2k}) = 1\) for each \(k\). The per-term identity and multipliability of both products give the result.
The \(z\)-dependent product admits a binary expansion as a double sum:
The product of \((1+a_n)(1+b_n)\) over \(n\) expands by choosing a subset \(P\) of indices contributing \(a_n\) and a subset \(N\) contributing \(b_n\). This uses the identities \(\prod (1+x_n) = \sum _{S\text{ finite}} \prod _{n\in S} x_n\) for each factor, combined via the product rule for infinite products.
Each term of the binary expansion has the explicit form
The \(q\)-exponents add up, and the \(z\)-powers contribute \(+1\) for each element of \(P\) and \(-1\) for each element of \(N\), giving \(z^{|P|-|N|}\).
For each \(d\in \mathbb {N}\), the \(q^d\)-coefficient of the double sum equals the \(q^d\)-coefficient of the state generating function:
The \(z\)-dependent product equals the state generating function:
Proof infrastructure for Jacobi’s triple product identity
The partition generating function \(\prod _{k{\gt}0}(1-q^{2k})^{-1}\in (\mathbb {Z}[z^{\pm }])[[q]]\) is a unit (its constant term is \(1\)).
The constant coefficient is \(1\), which is a unit.
The state generating function equals the RHS of Jacobi’s identity times the partition generating function:
Using the bijection \(\Phi _{\ell }\) from Theorem 2.92, we rewrite the sum over states as
The second factor is \(\prod _{n{\gt}0}(1-q^{2n})^{-1}\) by the generating function for partitions.
The state generating function equals the LHS of Jacobi’s identity times the partition generating function:
The proof chains the identities. By Lemma 2.110,
By Lemma 2.106, this equals
By Lemma 2.105, this equals
Parameterized Jacobi identity infrastructure
For integers \(a{\gt}0\) and rational \(u\), the evaluated partition generating function \(\prod _{k{\gt}0}(1-u^{2k}x^{2ak})^{-1}\in \mathbb {Q}[[x]]\) is a unit (its constant term is \(1\)).
The constant coefficient is \(1\), which is a unit in \(\mathbb {Q}\).
For \(a {\gt} 0\), the partition generating function times the Euler product (both evaluated at parameter \(a\), \(u\)) equals \(1\):
Per-factor cancellation: each geometric series factor \((1 + u^{2k}x^{2ak} + u^{4k}x^{4ak} + \cdots )\) multiplied by \((1 - u^{2k}x^{2ak})\) gives \(1\). The proof stabilizes the partial products and shows the coefficients eventually agree.
The product of the RHS of Jacobi’s identity (evaluated at \(q=ux^a\), \(z=vx^b\)) with the partition generating function equals the state generating function:
Follows from the Cauchy product formula for infinite sums.
The product of the LHS of Jacobi’s identity (evaluated at \(q=ux^a\), \(z=vx^b\)) with the partition generating function equals the state generating function.
Jacobi implies Euler
For any \(\ell \in \mathbb {Z}\),
Direct computation: \(3\ell ^{2}+\ell = (3\ell +1)\ell = (3(-\ell )-1)(-\ell ) = 2w_{-\ell }\).
Let \(K\) be a commutative ring. Let \(f\) and \(g\) be two FPSs in \(K[[x]]\). Assume that \(f[x^{2}]=g[x^{2}]\). Then, \(f=g\).
Write \(f=\sum _{n\in \mathbb {N}}f_{n}x^{n}\) and \(g=\sum _{n\in \mathbb {N}}g_{n}x^{n}\). Then \(f[x^{2}]=\sum _{n\in \mathbb {N}}f_{n}x^{2n}\) and \(g[x^{2}]=\sum _{n\in \mathbb {N}}g_{n}x^{2n}\). Comparing \(x^{2n}\)-coefficients in \(f[x^{2}]=g[x^{2}]\) yields \(f_{n}=g_{n}\) for each \(n\in \mathbb {N}\). Hence \(f=g\).
The LHS of Jacobi’s identity evaluated at \(a=3\), \(b=1\), \(u=1\), \(v=-1\) equals \(\prod _{k{\gt}0}(1-x^{k})[x^{2}]\), i.e. the Euler product with \(x\) replaced by \(x^{2}\):
The LHS factors simplify: setting \(q=x^{3}\), \(z=-x\) gives factors \((1-x^{6n-2})(1-x^{6n-4})(1-x^{6n})\) for each \(n{\gt}0\), which is \(\prod _{k{\gt}0}(1-(x^{2})^{k})\).
The RHS of Jacobi’s identity evaluated at \(a=3\), \(b=1\), \(u=1\), \(v=-1\) equals the pentagonal series with \(x\) replaced by \(x^{2}\):
The RHS sum is \(\sum _{\ell \in \mathbb {Z}}(-1)^{\ell }x^{3\ell ^{2}+\ell }\). By Lemma 2.118, \(3\ell ^{2}+\ell =2w_{-\ell }\), so the exponents are all even and the sum equals \(\sum _{k\in \mathbb {Z}}(-1)^{k}(x^{2})^{w_{k}}\), which is the pentagonal series evaluated at \(x^{2}\).
Euler’s pentagonal number theorem holds over \(\mathbb {Q}\):
The coefficients of the Euler product are preserved by the ring homomorphism \(\mathbb {Z}\to \mathbb {Q}\):
where \(\iota :\mathbb {Z}\hookrightarrow \mathbb {Q}\) is the inclusion.
The ring homomorphism \(\mathbb {Z}\to \mathbb {Q}\) sends the \(\mathbb {Z}\)-product to the \(\mathbb {Q}\)-product by continuity of the induced map on power series, and coefficients commute with the map.
Application: A recursion for the sum of divisors
We have \(P\cdot Q = 1\), where \(P=\sum _{n\geq 0}p(n)x^{n}\) is the partition generating function and \(Q=\sum _{k\in \mathbb {Z}}(-1)^{k}x^{w_{k}}\) is the pentagonal series.
The sum-of-divisors generating function is
where \(\sigma (k) = \sigma _1(k) = \sum _{d\mid k} d\) is the sum of positive divisors of \(k\).
- AlgebraicCombinatorics.sigmaSeries = PowerSeries.mk fun (n : ℕ) => if n = 0 then 0 else ↑((ArithmeticFunction.sigma 1) n)
For each \(n\in \mathbb {N}\),
The proof uses a combinatorial double-counting argument: a marked partition \((p, i)\) (a partition \(p\) of \(n\) together with a marked cell \(i\in \{ 1,\ldots ,n\} \)) can equivalently be described by \((d, m, j, \mu )\) where \(d\) is the row length of the marked cell, \(m\) is the number of rows of length \(d\), \(j\) is the column of the cell, and \(\mu \) is the partition obtained by removing all rows of length \(d\). The identity follows by summing \(\sum _{k=1}^n \sigma (k) p(n-k) = \sum _{d\mid k} d \cdot p(n-k)\) and reindexing.
We have \(xP'=SP\), where \(P\) is the partition generating function and \(S=\sum _{k{\gt}0}\sigma (k)x^{k}\) is the sum-of-divisors generating function.
Both sides have the same coefficients: the coefficient of \(x^{n}\) on the left is \(n\cdot p(n)\), and on the right is \(\sum _{k=1}^{n}\sigma (k)\cdot p(n-k)\). These are equal by the combinatorial identity (Lemma 2.126).
We have \(xQ'=-QS\), where \(Q\) is the pentagonal series and \(S\) is the sum-of-divisors generating function.
From \(PQ=1\), differentiate to get \(P'Q+PQ'=0\), so \(PQ'=-P'Q\). Multiply by \(x\): \(xPQ'=-xP'Q=-SPQ=-S\) (using \(xP'=SP\) and \(PQ=1\)). Since \(PQ=1\) is a unit, multiply both sides by \(Q\) to get \(xQ'=-QS\).
The \(n\)-th coefficient of \(xQ'\) is determined by pentagonal numbers:
This follows from \(xQ' = \sum _{k\in \mathbb {Z}} (-1)^k w_k x^{w_k}\).
For any positive integer \(n\), let \(\sigma (n)\) denote the sum of all positive divisors of \(n\).
Then, for each positive integer \(n\), we have
(Here, \(w_{k}\) is the \(k\)-th pentagonal number, defined in Definition 2.67.)
From Lemma 2.128, we have \(xQ'=-QS\), where \(Q=\sum _{k\in \mathbb {Z}}(-1)^{k}x^{w_{k}}\) and \(S=\sum _{k{\gt}0}\sigma (k)x^{k}\).
Taking the derivative:
On the other hand:
Comparing the coefficient of \(x^{n}\) on both sides:
On the left, the coefficient is \((-1)^{k}w_{k}\) if \(n=w_{k}\) for some \(k\), and \(0\) otherwise (Lemma 2.129);
On the right, the coefficient is \(\sum _{\substack{[k, \in , \mathbb , {, Z, }, ;, \\ , w, _, {, k, }, {\lt}, n]}}(-1)^{k-1}\sigma (n-w_{k})\).
Rearranging gives the result.
Alternative proof via evaluation homomorphism
The evaluation map from \((\mathbb {Z}[z^{\pm }])[[q]]\) to \(\mathbb {Q}[[x]]\) is defined by sending a power series \(f = \sum _e c_e q^e\) (where \(c_e \in \mathbb {Z}[z^{\pm }]\)) to
where \(\widehat{c_e}(a,b,v,e)\) denotes the shifted evaluation that replaces each \(z^\ell \) in \(c_e\) by \(v^\ell x^{ae+b\ell }\).
- AlgebraicCombinatorics.evalJacobiCorrect a b u v f = ∑' (e : ℕ), u ^ e • AlgebraicCombinatorics.evalLaurentCoeffShifted a b v e ((PowerSeries.coeff e) f)
Evaluating the RHS of Jacobi’s identity gives the parameterized RHS:
Each sum term \(q^{\ell ^2}z^\ell \) is evaluated to \(u^{\ell ^2} v^\ell x^{a\ell ^2+b\ell }\). The evaluation distributes over the infinite sum by summability and continuity.