CorollaryStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)audited 2026-08-28

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.

Partitions with at most k parts are equinumerous with partitions whose parts are all at most k

Statement

For every $n \geq 0$ and $k \geq 0$ , the number of partitions of $n$ with at most $k$ parts equals the number of partitions of $n$ whose parts are all at most $k$ .

Facts & Assumptions

Given: integers $n \geq 0$ and $k \geq 0$ .

[F1]

A partition has all parts at most $k$ exactly when its largest part is at most $k$ (The functions p(n), p_k(n), and the standard restricted partition families).

[L1]

For each $j \geq 0$ , partitions with exactly $j$ parts are equinumerous with partitions whose largest part is $j$ (Partitions with k parts are equinumerous with partitions whose largest part is k).

Proof

technique · bijection

1.1

Let $λ$ be a partition of $n$ with at most $k$ parts. If $λ$ has exactly $j$ parts, then $j \leq k$ , and [L1] sends $λ$ by conjugation to a partition whose largest part is $j$ . By [F1], every part of the conjugate is therefore at most $k$ . The same reasoning in reverse sends any partition all of whose parts are at most $k$ to one with at most $k$ parts.

F1L1

2.1

Thus conjugation restricts to a bijection between the two displayed sets, so they have equal cardinality.

step 1.1∎

Depends on

Used by

Dependency tree · two levels

5 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)