Pentagonal Number Theorem — Lemmas

This file contains the key lemmas for the Pentagonal Number Theorem, following Franklin's involution argument.

Main results

• distinct_parts_disjoint_union: the partition classes α/β/special are disjoint with union
• special_partition_char: characterization of special partitions
• franklin_involution_bijection: Franklin's involution is a bijection
• parity_flip: Franklin's involution flips even/odd parity
• signed_partition_main: pe(n) - po(n) = (-1)^k for pentagonal n, 0 otherwise

theorem DPalpha_inter_DPbeta (n : ℕ) : distinctPartitionsAlpha n ∩ distinctPartitionsBeta n = ∅

α-partitions and β-partitions are disjoint.

theorem DPalpha_inter_DPspecial (n : ℕ) : distinctPartitionsAlpha n ∩ distinctPartitionsSpecial n = ∅

α-partitions and special partitions are disjoint.

theorem DPbeta_inter_DPspecial (n : ℕ) : distinctPartitionsBeta n ∩ distinctPartitionsSpecial n = ∅

β-partitions and special partitions are disjoint.

theorem DP_eq_union (n : ℕ) : distinctPartitions n = distinctPartitionsAlpha n ∪ distinctPartitionsBeta n ∪ distinctPartitionsSpecial n

Every distinct partition is in exactly one of α, β, or special.

theorem mul_three_sub_one_add_self (a : ℕ) : a * (3 * a - 1) + a = 3 * a ^ 2

The pentagonal identity a * (3 * a - 1) = 3 * a ^ 2 - a, stated without truncated subtraction so that omega can use it.

theorem SmkSet_card (k : ℕ) (hk : 1 ≤ k) : (smkSet k).card = k

The set smkSet(k) has exactly k elements.

theorem SmkSet_sum (k : ℕ) (hk : 1 ≤ k) : (smkSet k).sum id = (3 * k ^ 2 - k) / 2

The sum of smkSet(k) equals (3k²-k)/2.

theorem SpkSet_card (k : ℕ) (hk : 1 ≤ k) : (spkSet k).card = k

The set spkSet(k) has exactly k elements.

theorem SpkSet_sum (k : ℕ) (hk : 1 ≤ k) : (spkSet k).sum id = (3 * k ^ 2 + k) / 2

The sum of spkSet(k) equals (3k²+k)/2.

theorem DP_eq_Icc_of_run_reaches_base (S : Finset ℕ) (hne : S.Nonempty) (h : partMax S - partSlope S + 1 ≤ partBase S) : S = Finset.Icc (partBase S) (partMax S)

A nonempty distinct partition whose top run reaches all the way down to its base is the whole interval Icc (partBase S) (partMax S).

theorem DPspecial_eq_Icc (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsSpecial n) (hne : S.Nonempty) : S = Finset.Icc (partBase S) (partMax S) ∧ partSlope S = partMax S - partBase S + 1 ∧ 2 * n = partSlope S * (partBase S + partMax S)

A nonempty special partition of n is exactly the interval Icc b m running from its base b to its max m. Consequently its slope is the full length m - b + 1 of that interval, and 2 * n = s * (b + m) by Gauss' summation formula.

theorem DPspecial_empty_of_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) : distinctPartitionsSpecial n = ∅

For non-pentagonal n ≥ 1, there are no special partitions.

theorem pent_minus_inj {a b : ℕ} (h : 3 * a ^ 2 + b = 3 * b ^ 2 + a) : a = b

x ↦ 3x² − x is injective on ℕ, stated without truncated subtraction.

theorem pent_plus_ne_pent_minus {j k : ℕ} (hk : 1 ≤ k) (h : 3 * j ^ 2 + j + k = 3 * k ^ 2) : False

The two pentagonal families never collide: 3j² + j ≠ 3k² − k when 1 ≤ k.

theorem DPspecial_pent_minus (n k : ℕ) (hk : 1 ≤ k) (hn : 2 * n = 3 * k ^ 2 - k) : distinctPartitionsSpecial n = {smkSet k}

For n = (3k²-k)/2 (pentagonal minus), the only special partition is smkSet(k).

theorem partBase_spkSet {k : ℕ} (hk : 1 ≤ k) : partBase (spkSet k) = k + 1

The base of spkSet k is k + 1.

theorem partMax_spkSet {k : ℕ} (hk : 1 ≤ k) : partMax (spkSet k) = 2 * k

The largest part of spkSet k is 2 * k.

theorem partSlope_spkSet {k : ℕ} (hk : 1 ≤ k) : partSlope (spkSet k) = k

spkSet k is one single run, so its slope is its whole length k.

theorem pent_plus_inj {a b : ℕ} (h : a * (3 * a + 1) = 3 * b ^ 2 + b) : a = b

The pentagonal numbers of the second kind are pairwise distinct: a ↦ a * (3 * a + 1) is injective.

theorem pent_minus_ne_pent_plus (c b : ℕ) : (c + 1) * (3 * c + 2) ≠ 3 * b ^ 2 + b

No pentagonal number of the first kind is also one of the second kind: with a = c + 1, a * (3 * a - 1) = (c + 1) * (3 * c + 2) never equals b * (3 * b + 1).

theorem DPspecial_pent_plus (n k : ℕ) (hk : 1 ≤ k) (hn : 2 * n = 3 * k ^ 2 + k) : distinctPartitionsSpecial n = {spkSet k}

For n = (3k²+k)/2 (pentagonal plus), the only special partition is spkSet(k).

theorem alphaOp_mem_DPbeta (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : alphaOp S ∈ distinctPartitionsBeta n

The Franklin α-operation maps α-partitions into β-partitions.

theorem betaOp_mem_DPalpha (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : betaOp S ∈ distinctPartitionsAlpha n

The Franklin β-operation maps β-partitions into α-partitions.

theorem betaOp_alphaOp (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : betaOp (alphaOp S) = S

The β-operation is a left inverse of the α-operation.

theorem alphaOp_betaOp (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : alphaOp (betaOp S) = S

The α-operation is a left inverse of the β-operation.

theorem alphaOp_inj (n : ℕ) {S T : Finset ℕ} (hS : S ∈ distinctPartitionsAlpha n) (hT : T ∈ distinctPartitionsAlpha n) (h : alphaOp S = alphaOp T) : S = T

alphaOp is injective on distinctPartitionsAlpha n, since betaOp is a left inverse.

theorem DPalpha_card_eq_DPbeta_card (n : ℕ) : (distinctPartitionsAlpha n).card = (distinctPartitionsBeta n).card

Franklin's involution gives a bijection: |α(n)| = |β(n)|.

theorem alphaOp_card (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : (alphaOp S).card + 1 = S.card

The α-operation preserves the number of parts.

theorem betaOp_card (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : (betaOp S).card = S.card + 1

The β-operation preserves the number of parts.

theorem DPalpha_filter_card_eq (n : ℕ) (p q : ℕ → Prop) [DecidablePred p] [DecidablePred q] (hpq : ∀ (a : ℕ), p (a + 1) ↔ q a) : {S ∈ distinctPartitionsAlpha n | p S.card}.card = {S ∈ distinctPartitionsBeta n | q S.card}.card

Franklin's involution refined by a condition on the number of parts: α matches the members of 𝒫_α(n) whose size satisfies p with those of 𝒫_β(n) whose size satisfies q, provided p (a + 1) and q a always agree (recall |α(S)| + 1 = |S|).

theorem DPalpha_odd_card_eq_DPbeta_even_card (n : ℕ) : {S ∈ distinctPartitionsAlpha n | S.card % 2 = 1}.card = {S ∈ distinctPartitionsBeta n | S.card % 2 = 0}.card

|{S ∈ α(n) : |S| odd}| = |{S ∈ β(n) : |S| even}|.

theorem DPalpha_even_card_eq_DPbeta_odd_card (n : ℕ) : {S ∈ distinctPartitionsAlpha n | S.card % 2 = 0}.card = {S ∈ distinctPartitionsBeta n | S.card % 2 = 1}.card

|{S ∈ α(n) : |S| even}| = |{S ∈ β(n) : |S| odd}|.

theorem DP_card_filter_split (n : ℕ) (P : Finset ℕ → Prop) [DecidablePred P] : (Finset.filter P (distinctPartitions n)).card = (Finset.filter P (distinctPartitionsAlpha n)).card + (Finset.filter P (distinctPartitionsBeta n)).card + (Finset.filter P (distinctPartitionsSpecial n)).card

Any filtered count of distinctPartitions n splits along the α/β/special decomposition.

theorem pe_minus_po_eq_special (n : ℕ) : ↑(pe n) - ↑(po n) = ↑{S ∈ distinctPartitionsSpecial n | S.card % 2 = 0}.card - ↑{S ∈ distinctPartitionsSpecial n | S.card % 2 = 1}.card

pe(n) - po(n) equals the signed count of special partitions.

theorem pe_minus_po_zero : ↑(pe 0) - ↑(po 0) = 1

Lemma 24 (Source), case n = 0: p_e(0) − p_o(0) = 1.

theorem pe_minus_po_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) : ↑(pe n) - ↑(po n) = 0

For non-pentagonal n ≥ 1, pe(n) - po(n) = 0.

theorem signed_card_of_singleton (T : Finset ℕ) (k : ℕ) (hT : T.card = k) : ↑{S ∈ {T} | S.card % 2 = 0}.card - ↑{S ∈ {T} | S.card % 2 = 1}.card = (-1) ^ k

The signed count of a one-element family of partitions with k parts is (-1) ^ k.

theorem pe_minus_po_pent_minus (n k : ℕ) (hk : 1 ≤ k) (hn : 2 * n = 3 * k ^ 2 - k) : ↑(pe n) - ↑(po n) = (-1) ^ k

For n = (3k²-k)/2, pe(n) - po(n) = (-1)^k.

theorem pe_minus_po_pent_plus (n k : ℕ) (hk : 1 ≤ k) (hn : 2 * n = 3 * k ^ 2 + k) : ↑(pe n) - ↑(po n) = (-1) ^ k

For n = (3k²+k)/2, pe(n) - po(n) = (-1)^k.