How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Durfee-square decomposition of the partition series
Statement
In ,
where the empty product at is .
Facts & Assumptions
Given: partitions written by Ferrers diagrams.
Two formal series are equal exactly when their coefficients agree (Coefficient extraction is -linear, separates formal series, shifts under multiplication by , and converts products to finite convolution).
Partitions with at most parts are equinumerous with partitions whose parts are all at most (Partitions with at most k parts are equinumerous with partitions whose parts are all at most k).
Proof
Let be a partition with Durfee length . Removing its Durfee square leaves two pieces: a right-hand piece consisting of the cells to the right of the square, and a lower piece consisting of the cells below the square. The piece has at most rows, while each row of has length at most . Conversely, given , a partition with at most parts, and a partition with all parts at most , one reconstructs uniquely by adjoining to the right side and below the square.
For fixed , the square contributes the factor . By [L2], the right-hand piece has the same generating function as partitions with parts at most , namely ; the lower piece has the same generating function for the same direct multiplicity reason. Thus partitions whose Durfee square has size contribute .
Every partition has exactly one Durfee length, so summing the contributions of step 2.1 over all counts every partition exactly once. Therefore the coefficient of on the right is for every , and [L1] gives the displayed identity.
Depends on
- Ferrers and Young diagrams, conjugate partitions, self-conjugacy, and the Durfee square
- Partitions with at most k parts are equinumerous with partitions whose parts are all at most k
- Integer partitions have generating function $\prod_{n\ge 1}(1-x^n)^{-1}$
- Coefficient extraction is $R$-linear, separates formal series, shifts under multiplication by $x^k$, and converts products to finite convolution
Used by
Dependency tree · two levels
12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Stephen Melczer, An Invitation to Enumeration, Chapter 9: Integer Partitions (standard reference, not scraped)