feat(partitions): generalized pentagonal numbers.

[BeibeiX0]

feat(partitions): generalized pentagonal numbers and error term eₙ

Introduce infrastructure around Euler’s pentagonal number theorem:

• Define parity counters for strict partitions:

  • p_even_distinct n
  • p_odd_distinct n
  • strict_partitions_parity_diff n := (p_even_distinct n : ℤ) - (p_odd_distinct n : ℤ)

• Generalized pentagonal numbers:

  • generalizedPentagonalZ : ℤ → ℤ with basic API (gpn_nonneg, gpn_coe)
  • generalizedPentagonalNum : ℤ → ℕ
  • parity lemma even_neg_j_add_three_j_sq and even_neg_j_add_three_j_sq'
  • search window equivalence exists_j_iff_exists_j_in_range
  • Decidable (∃ j : ℤ, n = generalizedPentagonalZ j) via a bounded range

• Euler error term:

  • error_term_e n : ℤ (≔ (-1)^{|j|} if n = generalizedPentagonalZ j for some j,
    and 0 otherwise)

• Finite product cut-off of the generating function:

  • E n : PowerSeries ℤ := ∏_{k=1}^{n+1} (1 - X^k)
  • lemma coeff_E_eq_coeff_cutoff

Implementation notes:

• Keep the integer-valued version generalizedPentagonalZ for arithmetic lemmas and
  signs; obtain the natural-number version via Int.toNat.
• The bounded search lemma gives a small window j ∈ [-(n+1), n+1] for decidability.

Motivation:

• This is groundwork for proofs of Euler’s pentagonal number theorem and parity
  identities relating strict partitions to the error term.

References:

• https://en.wikipedia.org/wiki/Pentagonal_number_theorem

[github-actions]

PR summary 50468bbd01

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.Enumerative.PentagonalNumbers (new file)	1505

---

Declarations diff

+ E
+ coeff_E_eq_coeff_cutoff
+ error_term_e
+ even_neg_j_add_three_j_sq
+ even_neg_j_add_three_j_sq'
+ exists_j_iff_exists_j_in_range
+ generalizedPentagonalNum
+ generalizedPentagonalZ
+ gpn_coe
+ gpn_nonneg
+ instance (n : ℕ) : Decidable (∃ j : ℤ, n = generalizedPentagonalZ j)
+ p_even_distinct
+ p_odd_distinct
+ strict_partitions_parity_diff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[wwylele]

Hi, glad to see someone who is also interested in the pentagonal number theorem! I am actually in the process of upstreaming my formalization of the same theorem from https://github.com/wwylele/PentagonalNumberTheorem, and I am currently building the generating functions in #30567. Meanwhile, I didn't define the term generalizedPentagonalZ or much API for it (and just kept all the expanded formula everywhere), so I am happy to see more useful lemma for it. How do you think about a collaboration?

[BeibeiX0]

Hi, glad to see someone who is also interested in the pentagonal number theorem! I am actually in the process of upstreaming my formalization of the same theorem from https://github.com/wwylele/PentagonalNumberTheorem, and I am currently building the generating functions in #30567. Meanwhile, I didn't define the term generalizedPentagonalZ or much API for it (and just kept all the expanded formula everywhere), so I am happy to see more useful lemma for it. How do you think about a collaboration?

It’s awesome to hear that you’re working on the formalization of the Pentagonal Number Theorem!
As for collaboration, I think it would be a great opportunity to work together. I can help with formalizing the generalizedPentagonalZ term or building out more API functions and lemmas that could be useful for future work. I’d be interested in expanding on the existing formalization to ensure that the important properties and relations are covered comprehensively.
If you have specific tasks or areas that you’d like to collaborate on, feel free to share! I’d love to help out and contribute where needed.