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.

noncomputable def p_count (n : ℕ) : ℕ

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

• p_count n = Fintype.card n.Partition

noncomputable def pGenFun : PowerSeries ℤ

The generating function for p_count: a formal power series in ℤ⟦X⟧ whose coefficients are the partition counts.

Equations

• pGenFun = Nat.Partition.genFun fun (x x_1 : ℕ) => 1

theorem coeff_pGenFun_eq_p_count (n : ℕ) : (PowerSeries.coeff n) pGenFun = ↑(p_count n)

Lemma 3 (combinatorial side). The n-th coefficient of the partition generating function is p(n).

theorem pGenFun_eq_prod : pGenFun = ∏' (i : ℕ), (1 + ∑' (j : ℕ), 1 • PowerSeries.X ^ ((i + 1) * (j + 1)))

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).

theorem coeff_prod_neg_X_pow (n : ℕ) (T : Finset ℕ) : (PowerSeries.coeff n) (∏ k ∈ T, -PowerSeries.X ^ k) = if T.sum id = n then (-1) ^ T.card else 0

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}.

theorem coeff_prod_eq_signed_partition_sum (n : ℕ) : (PowerSeries.coeff n) (∏ k ∈ Finset.Icc 1 n, (1 - PowerSeries.X ^ k)) = ∑ S ∈ distinctPartitions n, (-1) ^ S.card

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).

theorem signed_partition_sum_eq_pe_sub_po (n : ℕ) : ∑ S ∈ distinctPartitions n, (-1) ^ S.card = ↑(pe n) - ↑(po n)

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).

theorem coeff_prod_eq_pe_sub_po (n : ℕ) : (PowerSeries.coeff n) (∏ k ∈ Finset.Icc 1 n, (1 - PowerSeries.X ^ k)) = ↑(pe n) - ↑(po 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}.)

theorem coeff_prod_pentagonal_zero : (PowerSeries.coeff 0) (∏ k ∈ Finset.Icc 1 0, (1 - PowerSeries.X ^ k)) = 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.)

theorem coeff_prod_pentagonal_nonpent (n : ℕ) (hn : 1 ≤ n) (h1 : ∀ (k : ℕ), 1 ≤ k → 2 * n ≠ 3 * k ^ 2 - k) (h2 : ∀ (k : ℕ), 1 ≤ k → 2 * n ≠ 3 * k ^ 2 + k) : (PowerSeries.coeff n) (∏ k ∈ Finset.Icc 1 n, (1 - PowerSeries.X ^ k)) = 0

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.

theorem coeff_prod_pentagonal_minus (n k : ℕ) (hk : 1 ≤ k) (hn : 2 * n = 3 * k ^ 2 - k) : (PowerSeries.coeff n) (∏ k' ∈ Finset.Icc 1 n, (1 - PowerSeries.X ^ k')) = (-1) ^ k

PNT (Euler), pentagonal (3k²-k)/2 case. If 2n = 3k² - k for some k ≥ 1 (equivalently, n = (3k²-k)/2), then [X^n] ∏_{k'=1}^{n}(1 - X^{k'}) = (-1)^k.

theorem coeff_prod_pentagonal_plus (n k : ℕ) (hk : 1 ≤ k) (hn : 2 * n = 3 * k ^ 2 + k) : (PowerSeries.coeff n) (∏ k' ∈ Finset.Icc 1 n, (1 - PowerSeries.X ^ k')) = (-1) ^ k

PNT (Euler), pentagonal (3k²+k)/2 case. If 2n = 3k² + k for some k ≥ 1 (equivalently, n = (3k²+k)/2), then [X^n] ∏_{k'=1}^{n}(1 - X^{k'}) = (-1)^k.

theorem natCast_eq_gen_pent_div_two_iff (n : ℕ) (k : ℤ) : ↑n = k * (3 * k - 1) / 2 ↔ 2 * ↑n = k * (3 * k - 1)

k * (3 * k - 1) is always even, so over ℤ the generalized pentagonal equation n = k(3k-1)/2 is equivalent to its subtraction-free form 2n = k(3k-1).

theorem pe_minus_po_of_gen_pent (n : ℕ) (k : ℤ) (hk : 2 * ↑n = k * (3 * k - 1)) : ↑(pe n) - ↑(po n) = (-1) ^ k.natAbs

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.

theorem exists_gen_pent_of_pent (n j : ℕ) (hj : 1 ≤ j) (h : 2 * n = 3 * j ^ 2 - j ∨ 2 * n = 3 * j ^ 2 + j) : ∃ (k : ℤ), 2 * ↑n = k * (3 * k - 1)

Converse bookkeeping: both ℕ-indexed pentagonal families 2n = 3j² ∓ j (with j ≥ 1) produce an integer index k with 2n = k(3k-1), namely k = j and k = -j.

theorem euler_pentagonal_number_theorem_packaged (n : ℕ) : (∃ (k : ℤ), ↑n = k * (3 * k - 1) / 2 ∧ ↑(pe n) - ↑(po n) = (-1) ^ k.natAbs) ∨ (¬∃ (k : ℤ), ↑n = k * (3 * k - 1) / 2) ∧ ↑(pe n) - ↑(po n) = 0

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.