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, ….

Lean proofpassed
Unfinished proof stepsNone
Formal resultAccepted
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.

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.

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

Paired partition-diagram forms connected by alternating solid and dashed contribution arcs at the sparse generalized-pentagonal offsets.
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.

Proof architecture

How Euler's product becomes the partition recurrence

5 curated 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 source-anchored stages explain the retained proof route. They are not an extracted Lean proof-term dependency graph.

  1. A procession of engraved Young diagrams enters an infinite forest-green product loom and collapses to one neutral antique-gold constant tile.
    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. A forest-green Euler-product loom releases alternating antique-gold gamma ribbons at sparse landings while one translucent cobalt tail veil continues beyond the finite expansion.
    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. A cobalt coefficient lens fixes one finite coefficient horizon while a sparse paired staircase grows beyond it and the translucent remainder veil recedes into the distance.
    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. A cobalt lens selects one coefficient slot from two series, unfolds their product down a single antidiagonal grid, separates the current Young diagram, and preserves only sparse paired survivors.
    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. Five sparse curved landings hold paired earlier Young diagrams with alternating solid gold and hatched green rims, and their contribution ribbons reconstruct one larger current Young diagram.
    Earlier partition numbers at paired generalized-pentagonal offsets reconstruct p(n), with signs alternating in pairs and only finitely many eligible terms.
    05

    Paired pentagonal offsets reconstruct p(n)

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

    Moving the nonzero product terms to the other side changes -pentagonalSign(k) to pentagonalSign(k). Only earlier partition numbers at generalized-pentagonal offsets remain; the offsets occur in pairs, their signs alternate by pair, and g(k) ≤ n makes the recurrence finite.

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

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

Result boundary

What this page 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.

Continue the mathematics

Start from the complete checked source

The pinned theorem and its complete local import closure let internal and external agents inspect the proof, compare an alternate route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks every proposed extension against its exact formal statement.

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

Checked source + agent continuation package · 1 Lean file · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Formal-result publication and review details

Independent publication review

The formal theorem's publication gates are accepted

Lean checks the proof. Independent AI review separately accepted evidence completeness, statement alignment, result boundary, and the retained theorem wording. Those gates apply to the formal result; generated media is reviewed and promoted separately. Neither review replaces Lean's proof check or broadens the theorem.

01

Formal evidence

Independent 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

Independent 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 in a new tab