Pentagonal Number Theorem — Definitions

Core definitions for the formalization of the Euler Pentagonal Number Theorem via Franklin's involution.

Main definitions

• consecutiveTopRun: length of the maximal consecutive run ending at m in S
• distinctPartitions: partitions of n into distinct positive parts
• distinctPartitionsEven, distinctPartitionsOdd: partitions with an even (resp. odd) number of parts
• pe, po: cardinalities of distinctPartitionsEven n, distinctPartitionsOdd n
• partBase, partMax, partSlope, partSlopeSet: structural invariants of a partition
• distinctPartitionsAlpha, distinctPartitionsBeta, distinctPartitionsSpecial: three-way decomposition of distinctPartitions n by Franklin's involution
• smkSet, spkSet: the special pentagonal partitions S_{−k} and S_k
• alphaOp, betaOp: Franklin's involution maps on distinctPartitionsAlpha and distinctPartitionsBeta

def consecutiveTopRun (S : Finset ℕ) : ℕ → ℕ

The length of the maximal consecutive run of elements of S ending at m, counted downward.

Equations

• consecutiveTopRun S 0 = if 0 ∈ S then 1 else 0
• consecutiveTopRun S m.succ = if m + 1 ∈ S then 1 + consecutiveTopRun S m else 0

def distinctPartitions (n : ℕ) : Finset (Finset ℕ)

The set of subsets S ⊆ {1, …, n} with ∑_{s ∈ S} s = n, i.e., partitions of n into distinct positive parts.

Equations

• distinctPartitions n = {S ∈ (Finset.Icc 1 n).powerset | S.sum id = n}

def distinctPartitionsEven (n : ℕ) : Finset (Finset ℕ)

Partitions of n into distinct positive parts with an even number of parts.

Equations

• distinctPartitionsEven n = {S ∈ distinctPartitions n | S.card % 2 = 0}

def distinctPartitionsOdd (n : ℕ) : Finset (Finset ℕ)

Partitions of n into distinct positive parts with an odd number of parts.

Equations

• distinctPartitionsOdd n = {S ∈ distinctPartitions n | S.card % 2 = 1}

def pe (n : ℕ) : ℕ

Number of partitions of n into an even number of distinct positive parts.

Equations

• pe n = (distinctPartitionsEven n).card

def po (n : ℕ) : ℕ

Number of partitions of n into an odd number of distinct positive parts.

Equations

• po n = (distinctPartitionsOdd n).card

def partBase (S : Finset ℕ) : ℕ

The smallest element of a partition, returning 0 for the empty set.

Equations

• partBase S = if h : S.Nonempty then S.min' h else 0

def partMax (S : Finset ℕ) : ℕ

The largest element of a partition, returning 0 for the empty set.

Equations

• partMax S = if h : S.Nonempty then S.max' h else 0

def partSlope (S : Finset ℕ) : ℕ

The length of the maximal consecutive run from max(S) downward in S.

Equations

• partSlope S = consecutiveTopRun S (partMax S)

def partSlopeSet (S : Finset ℕ) : Finset ℕ

The interval {max(S) − slope(S) + 1, …, max(S)} (the "slope set" of S).

Equations

• partSlopeSet S = Finset.Icc (partMax S - partSlope S + 1) (partMax S)

def distinctPartitionsAlpha (n : ℕ) : Finset (Finset ℕ)

Partitions S ∈ distinctPartitions n that are nonempty and satisfy (b ≤ s ∧ b ∉ D) ∨ b + 1 ≤ s, with b = partBase S, s = partSlope S.

Equations

• distinctPartitionsAlpha n = {S ∈ distinctPartitions n | 0 < S.card ∧ (partBase S ≤ partSlope S ∧ ¬partMax S - partSlope S + 1 ≤ partBase S ∨ partBase S + 1 ≤ partSlope S)}

def distinctPartitionsBeta (n : ℕ) : Finset (Finset ℕ)

Partitions S ∈ distinctPartitions n that are nonempty and satisfy (s < b ∧ b ∉ D) ∨ s + 2 ≤ b, with b = partBase S, s = partSlope S.

Equations

• distinctPartitionsBeta n = {S ∈ distinctPartitions n | 0 < S.card ∧ (partSlope S < partBase S ∧ ¬partMax S - partSlope S + 1 ≤ partBase S ∨ partSlope S + 2 ≤ partBase S)}

def distinctPartitionsSpecial (n : ℕ) : Finset (Finset ℕ)

Partitions of n into distinct parts that are either empty or satisfy base(S) ∈ slopeSet(S) with base(S) = slope(S) or base(S) = slope(S) + 1.

Equations

• distinctPartitionsSpecial n = {S ∈ distinctPartitions n | S.card = 0 ∨ 0 < S.card ∧ partMax S - partSlope S + 1 ≤ partBase S ∧ (partBase S = partSlope S ∨ partBase S = partSlope S + 1)}

def smkSet (k : ℕ) : Finset ℕ

The pentagonal partition S_{−k} = {k, k+1, …, 2k−1} of (3k²−k)/2.

Equations

• smkSet k = Finset.Icc k (2 * k - 1)

def spkSet (k : ℕ) : Finset ℕ

The pentagonal partition S_k = {k+1, k+2, …, 2k} of (3k²+k)/2.

Equations

• spkSet k = Finset.Icc (k + 1) (2 * k)

def alphaOp (S : Finset ℕ) : Finset ℕ

For S ∈ 𝒫_α(n) with base b and max m, α(S) = (S \ {b, m−b+1}) ∪ {m+1}.

Equations

• alphaOp S = insert (partMax S + 1) ((S.erase (partBase S)).erase (partMax S - partBase S + 1))

def betaOp (S : Finset ℕ) : Finset ℕ

For S ∈ 𝒫_β(n) with slope s and max m, β(S) = (S ∪ {s, m−s}) \ {m}.

Equations

• betaOp S = (insert (partSlope S) (insert (partMax S - partSlope S) S)).erase (partMax S)