ProofAtlas

Partitions · formal theorem

Euler Pentagonal Recurrence

For every positive integer n, p(n) equals the exact finite alternating sum of earlier partition numbers at generalized pentagonal offsets 1, 2, 5, 7, ….

Scope: For every positive integer n, the checked statement gives the exact finite recurrence for p(n) using earlier partition numbers at generalized pentagonal offsets.

Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Euler pentagonal recurrence mapEach positive-index partition number is recovered from partition numbers at generalized pentagonal offsets, with alternating signs.
Exact scope: For every positive integer n, the checked statement gives the exact finite recurrence for p(n) using earlier partition numbers at generalized pentagonal offsets.

Exact formal proposition

Hypotheses and conclusion

This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.

def EulerPentagonalRecurrence : Prop :=
  ∀ n : Nat, 0 < n →
    (partitionNumber n : Int) =
      ∑ k ∈ pentagonalIndicesUpTo n,
        pentagonalSign k * (partitionNumber (n - generalizedPentagonalNat k) : Int)
Definitions used in this proposition

partitionNumber

def partitionNumber (n : Nat) : Nat :=
  Fintype.card (Nat.Partition n)

generalizedPentagonalNat

def generalizedPentagonalNat (k : Int) : Nat :=
  Int.toNat (generalizedPentagonal k)

pentagonalSign

def pentagonalSign (k : Int) : Int :=
  if Odd k.natAbs then 1 else -1

pentagonalIndicesUpTo

noncomputable def pentagonalIndicesUpTo (n : Nat) : Finset Int :=
  (Finset.Icc (-(n : Int)) (n : Int)).filter fun k =>
    k ≠ 0 ∧ 0 < generalizedPentagonal k ∧ generalizedPentagonal k ≤ (n : Int)
Lean wrapper declaration

The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.

theorem eulerPentagonalRecurrence :
    EulerPentagonalRecurrence
Open main Lean file

Proof route

How Euler's product becomes the partition recurrence

5 proof stages

The checked route starts with the partition generating function, expands Euler's product through a finite gamma-tail identity, removes the tail in formal power-series topology, and extracts one coefficient to obtain the paired generalized-pentagonal recurrence.

These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.

  1. Scientific figure illustrating: The partition generating function is the multiplicative inverse of Euler's product in formal power series.
    The partition generating function is the multiplicative inverse of Euler's product in formal power series.
    01

    Partitions invert the Euler product

    partitionGeneratingFunction · eulerProduct = 1

    In the formal power-series ring, the partition generating function is the multiplicative inverse of Euler's product. Their product is exactly one, so the argument uses coefficient identities rather than analytic convergence.

    Lean lemmas for this step
    • partitionNumber
    • coeff_partitionGeneratingFunction
    • hasProd_partitionGeneratingFunction
    • partitionGeneratingFunction_mul_eulerProduct
  2. Scientific figure illustrating: Repeated gamma recurrences produce a finite pentagonal partial sum while keeping one explicit remainder tail.
    Repeated gamma recurrences produce a finite pentagonal partial sum while keeping one explicit remainder tail.
    02

    Gamma terms telescope with a retained tail

    product = finite pentagonal partial sum + gamma tail

    Repeated applications of the gamma recurrence telescope into a finite generalized-pentagonal partial sum plus one explicit remainder. Retaining that tail makes the identity exact at every finite stage.

    Lean lemmas for this step
    • gamma
    • tail
    • tail_sub_tail
    • gamma_rec
    • product_eq_partial_sum
  3. Scientific figure illustrating: Increasing formal order removes the gamma tail coefficientwise, leaving Euler's product with coefficient sign -pentagonalSign(k), equivalently (-1)^k, at each generalized-pentagonal power.
    Increasing formal order removes the gamma tail coefficientwise, leaving Euler's product with coefficient sign -pentagonalSign(k), equivalently (-1)^k, at each generalized-pentagonal power.
    03

    Formal order removes the tail

    eulerProduct = Σ_{k∈ℤ} (-pentagonalSign(k)) · X^(generalizedPentagonal(k))

    For any fixed coefficient degree, the gamma tail eventually has formal order beyond that degree and contributes zero there. The resulting formal power-series expansion uses the Euler-product coefficient -pentagonalSign(k); this sign is reversed only later when the nonzero terms move across the coefficient identity.

    Lean lemmas for this step
    • product_eq_nat_sum
    • summable_gamma_powerSeries
    • pentagonal_product_nat_sum_powerSeries
    • pentagonal_product_intPos_sum_powerSeries
    • euler_product_pentagonal_expansion
  4. Scientific figure illustrating: Extracting a positive-degree coefficient separates p(n) from the sparse product coefficients -pentagonalSign(k) at nonzero generalized-pentagonal offsets.
    Extracting a positive-degree coefficient separates p(n) from the sparse product coefficients -pentagonalSign(k) at nonzero generalized-pentagonal offsets.
    04

    A positive coefficient unfolds antidiagonally

    p(n) + Σ_{k≠0, g(k)≤n} (-pentagonalSign(k)) · p(n−g(k)) = 0

    The positive-degree coefficient of the inverse-product identity is an antidiagonal convolution equal to zero. Its zero-offset term is p(n); every other surviving product coefficient is -pentagonalSign(k), exactly as in EulerPentagonalCoefficientIdentity.

    Lean lemmas for this step
    • product_identity_coeff_antidiagonal_zero
    • antidiagonal_sum_eq_partition_add_positive_coeffs
    • positive_coefficients_sum_eq_pentagonal_indices_sum
    • product_identity_implies_coefficient_identity
  5. Text-free Scientific diagram with three two-node groups feeding a single target; the groups carry positive, negative, positive sign pairs.
    Three paired groups of earlier terms, with signs +,+ then −,− then +,+, feed one finite recurrence target.
    05

    Three paired contributions converge on one target

    p(n) = Σ_{k≠0, g(k)≤n} pentagonalSign(k) · p(n−g(k))

    Six earlier-term nodes are enclosed in three pairs. Each node has its own arrow to a single target. The top and bottom pairs have positive signs; the middle pair has negative signs, expressing the alternating paired contribution pattern without printing a formula.

    Lean lemmas for this step
    • coefficient_identity_implies_recurrence
    • product_identity_implies_recurrence
    • eulerPentagonalRecurrence
    • generalizedPentagonal_one
    • generalizedPentagonal_neg_one
    • generalizedPentagonal_two
    • generalizedPentagonal_neg_two

The theorem at a glance

Euler's recurrence at a glance

Editorial poster for Euler's partition recurrence, with paired offsets 1,2; 5,7; 12,15, alternating paired signs, the exact finite recurrence, all seven partitions of five, four generating-function proof steps, and a recurrence-only scope footer.
Partition numbers recur only at generalized-pentagonal offsets, with signs in the rhythm +,+,−,−,+,+,….

Accessible transcript

p(n) = Σ_{k∈ℤ, k≠0, g(k)≤n} (−1)^(k+1) p(n−g(k)), g(k)=k(3k−1)/2

The partition generating function is the inverse of Euler's product. Expanding that product at generalized-pentagonal powers and comparing positive-degree coefficients yields the finite recurrence; for example, p(5) = p(4) + p(3) − p(0) = 7.

Read the complete poster transcript

PARTITIONS · GENERATING FUNCTIONS

EULER PENTAGONAL RECURRENCE

1, 2 · 5, 7 · 12, 15 · …

+ + − − + +

SPARSE OFFSETS · PAIRED SIGNS

FOR EVERY n > 0

p(n) = Σ (−1)ᵏ⁺¹ p(n − g(k))

k ∈ Z · k ≠ 0 · g(k) ≤ n

g(k) = k(3k − 1)/2

p(n) is the number of integer partitions of n.

TRY n = 5

p(5) = p(4) + p(3) − p(0) = 5 + 3 − 1 = 7

5 · 4+1 · 3+2 · 3+1+1 · 2+2+1 · 2+1+1+1 · 1+1+1+1+1

HOW THE PROOF MOVES

1 · ENCODE PARTITIONS

The coefficients of P(X) are p(n).

2 · MULTIPLY BY EULER'S PRODUCT

P(X) · ∏ₘ≥₁(1 − Xᵐ) = 1

3 · EXPAND AT PENTAGONAL POWERS

Only 1, 2, 5, 7, 12, 15, … survive.

4 · COMPARE COEFFICIENTS

Move the signed terms to obtain the recurrence.

EXACT SCOPE

The partition-number recurrence. Not every equivalent product formulation. Not an asymptotic formula for p(n).

Theorem schematic

Partitions recur at sparse paired offsets

Scientific figure illustrating: Euler's recurrence reconstructs p(n) from earlier partition numbers at offsets 1, 2, 5, 7, … with signs +,+,−,−,….
Euler's recurrence reconstructs p(n) from earlier partition numbers at offsets 1, 2, 5, 7, … with signs +,+,−,−,….

p(n) = Σ (−1)^(k+1) p(n−k(3k−1)/2) over nonzero eligible k

Only earlier partition numbers at generalized-pentagonal offsets contribute to p(n). Positive and negative integer indices produce the paired offsets 1, 2; 5, 7; 12, 15; …, and pentagonalSign alternates their contributions in pairs.

Result boundary

What this theorem does—and does not—establish

For every positive integer n, the checked statement gives the exact finite recurrence for p(n) using earlier partition numbers at generalized pentagonal offsets.

About these visual explanations

These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

Continue the mathematics

Open questions and extensions

The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.

What the source ZIP contains

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.

Complete checked Lean source · 1 Lean file · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Publication review

Review record

Publication reviews accepted

Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.

01

Formal evidence

The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.

02

Statement alignment

The formal declaration was accepted against the named theorem and its exact variant.

03

Result boundary

The accepted boundary keeps nearby stronger or commonly confused claims out of scope.

04

Public wording

The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.

05

Canonical source

The first-party source link is pinned to the checked package commit and exact Lean file.

06

Accepted result

A validated accepted-result record binds the four reviews to the checked formalization.

Expanded visual

Open original image