Pentagonal Number Theorem — Formal Power Series Statements #
This file contains the formal power series identities from the source document
"Pentagonal Number Theorem" by Jonathan Conrad, Paula Muermann, Maryna Viazovska (May 11, 2026).
These results connect the combinatorial content (proved in Lemmas.lean)
to the algebraic identities involving generating functions.
The unrestricted partition count p(n): the number of ways to write
n as a sum of positive integers (with repetition allowed, order ignored).
Equations
Instances For
The generating function for pCount: a formal power series in ℤ⟦X⟧
whose coefficients are the partition counts.
Equations
- PentagonalNumberTheorem.Franklin.pGenFun = Nat.Partition.genFun fun (x x_1 : ℕ) => 1
Instances For
Lemma 3 (combinatorial side). The n-th coefficient of the partition
generating function is p(n).
Lemma 3 (product side). The generating function equals the formal product
∏_{k≥1} (1 + X^k + X^{2k} + ...) (the geometric series expansion of each
(1 - X^k)^{-1}). The product is taken in the X-adic topology on ℤ⟦X⟧,
where it converges (each [X^n] only sees finitely many factors).
The coefficient of X^n in ∏_{k ∈ T} (-X^k) is (-1)^|T| if ∑_{k ∈ T} k = n,
and 0 otherwise: the product collapses to (-1)^|T| · X^{T.sum id}.
Lemma 5a (combinatorial expansion). The coefficient of X^n in the
truncated product ∏_{k=1}^{n}(1 - X^k) equals ∑_{S ∈ distinctPartitions n} (-1)^|S|.
Proof sketch. Rewrite each factor as 1 + (-X^k) and use the classical
expansion of a product of 1 + a_k over subsets (Finset.prod_one_add):
∏_{k ∈ {1,…,n}} (1 + (-X^k)) = ∑_{T ⊆ {1,…,n}} ∏_{k ∈ T} (-X^k)
= ∑_{T ⊆ {1,…,n}} (-1)^|T| · X^{T.sum id}.
Since coeff n is linear, coeff_prod_neg_X_pow turns the coefficient into a sum of
if T.sum id = n then (-1)^|T| else 0 over the powerset, and that is by definition the
sum over distinctPartitions n (Finset.sum_filter).
Lemma 5b (parity split). The signed partition sum equals p_e(n) - p_o(n).
The sum splits over the partition
distinctPartitions n = distinctPartitionsEven n ⊔ distinctPartitionsOdd n.
On distinctPartitionsEven, (-1)^|S| = 1; on distinctPartitionsOdd, (-1)^|S| = -1.
The two pieces give |distinctPartitionsEven| and -|distinctPartitionsOdd|,
i.e. p_e(n) and -p_o(n).
Lemma 5 (Source). For each n, the coefficient of X^n in the
truncated product ∏_{k=1}^{n}(1 - X^k) in ℤ⟦X⟧ equals p_e(n) - p_o(n).
(The truncation matches the infinite product ∏_{k≥1}(1 - X^k) on this
coefficient because factors with k > n are ≡ 1 mod X^{n+1}.)
PNT (Euler), zero case. [X^0] ∏_{k=1}^{0}(1 - X^k) = 1.
(The product is empty, so this is just coeff 0 1 = 1; we state it via
coeff_prod_eq_pe_sub_po for uniformity with the other cases.)
PNT (Euler), non-pentagonal case. For n ≥ 1 with 2n not of the
form 3k² - k nor 3k² + k for any k ≥ 1,
[X^n] ∏_{k=1}^{n}(1 - X^k) = 0.
Franklin/Euler in unified integer-index form. If 2n = k(3k-1) for some k : ℤ,
then p_e(n) - p_o(n) = (-1)^|k|. This subsumes the three pentagonal cases:
k = 0 forces n = 0, k = j > 0 gives 2n = 3j² - j, and k = -j < 0 gives
2n = 3j² + j.
PNT (Euler), Maryna's unified form. For every n, either n is a
generalized pentagonal number k(3k-1)/2 for some k ∈ ℤ — in which case
p_e(n) - p_o(n) = (-1)^|k| — or it is not, in which case the difference
vanishes.
This repackages the four cases (pe_minus_po_zero, pe_minus_po_pent_minus,
pe_minus_po_pent_plus, pe_minus_po_nonpent) under a single integer index:
k = 0 gives n = 0, k ≥ 1 gives the (3k²-k)/2 family, and k ≤ -1
(with m = |k|) gives the (3m²+m)/2 family. All the arithmetic lives in
natCast_eq_gen_pent_div_two_iff, pe_minus_po_of_gen_pent and
exists_gen_pent_of_pent; what is left here is pure case bookkeeping.