ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

Small partitions and the first dominance incomparability

Example

The partitions of $n$ , each paired with its conjugate, are as follows for $0 \leq n \leq 5$ :

$n = 0$ : the empty partition $\emptyset$ , with $\emptyset^{'} = \emptyset$ ;
$n = 1$ : $(1)$ , self-conjugate;
$n = 2$ : $(2)$ and $(1, 1)$ , with $(2)^{'} = (1, 1)$ ;
$n = 3$ : $(3)$ , $(2, 1)$ , $(1, 1, 1)$ , with $(3)^{'} = (1, 1, 1)$ and $(2, 1)^{'} = (2, 1)$ ;
$n = 4$ : $(4)$ , $(3, 1)$ , $(2, 2)$ , $(2, 1, 1)$ , $(1, 1, 1, 1)$ , with $(4)^{'} = (1, 1, 1, 1)$ , $(3, 1)^{'} = (2, 1, 1)$ and $(2, 2)^{'} = (2, 2)$ ;
$n = 5$ : $(5)$ , $(4, 1)$ , $(3, 2)$ , $(3, 1, 1)$ , $(2, 2, 1)$ , $(2, 1, 1, 1)$ , $(1, 1, 1, 1, 1)$ , with $(5)^{'} = (1, 1, 1, 1, 1)$ , $(4, 1)^{'} = (2, 1, 1, 1)$ , $(3, 2)^{'} = (2, 2, 1)$ and $(3, 1, 1)^{'} = (3, 1, 1)$ .

For every $n \leq 5$ the dominance order on the partitions of $n$ is a chain, namely $(5) ⊳ (4, 1) ⊳ (3, 2) ⊳ (3, 1, 1) ⊳ (2, 2, 1) ⊳ (2, 1, 1, 1) ⊳ (1, 1, 1, 1, 1)$ for $n = 5$ , and $(4) ⊳ (3, 1) ⊳ (2, 2) ⊳ (2, 1, 1) ⊳ (1, 1, 1, 1)$ for $n = 4$ , with the shorter chains for $n \leq 3$ . Dominance is therefore a total order on the partitions of each $n \leq 5$ . It first fails to be total at $n = 6$ , where the partitions $(4, 1, 1)$ and $(3, 3)$ are incomparable: their prefix sums $4, 5, 6$ and $3, 6, 6$ cross, and the conjugates $(3, 1, 1, 1)$ and $(2, 2, 2)$ of this pair are likewise incomparable.

Facts & Assumptions

Given: The partitions listed above for $0 \leq n \leq 5$ and the two partitions $(4, 1, 1)$ and $(3, 3)$ of $6$ .

[F1]

The conjugate partition $λ^{'}$ has parts $λ_{j}^{'} = # {i : λ_{i} \geq j}$ , the diagram $[λ^{'}]$ is the transpose of $[λ]$ , and conjugation is an involution (Partitions, English diagrams, and conjugation).

[F2]

$λ ⊵ μ$ means $\sum_{i \leq r} λ_{i} \geq \sum_{i \leq r} μ_{i}$ for every $r \geq 1$ , with each sequence padded by zeros beyond its parts; $⊵$ is a partial order, and $λ ⊳ μ$ means $λ ⊵ μ$ with $λ \neq μ$ (Dominance order on partitions).

[F3]

Conjugation reverses dominance: $λ ⊵ μ$ if and only if $μ^{'} ⊵ λ^{'}$ (Conjugation reverses dominance).

Verification

technique · direct

1.1

The six lists are complete: a partition of $n \leq 5$ whose largest part is $a$ is exactly a partition of $n - a$ with all parts at most $a$ , with the part $a$ adjoined, so running over $a = n, n - 1, \dots, 1$ recovers each list, and for $n = 5$ this gives $a = 5$ : $(5)$ ; $a = 4$ : $(4, 1)$ ; $a = 3$ : $(3, 2)$ and $(3, 1, 1)$ ; $a = 2$ : $(2, 2, 1)$ and $(2, 1, 1, 1)$ ; $a = 1$ : $(1, 1, 1, 1, 1)$ , exactly the seven partitions displayed, with the same recursion for $n \leq 4$ .

givenF1

1.2

Each displayed conjugate is read off as the column-height sequence of the diagram: $(4, 1)$ has column heights $2, 1, 1, 1$ , so $(4, 1)^{'} = (2, 1, 1, 1)$ ; $(3, 2)$ has column heights $2, 2, 1$ , so $(3, 2)^{'} = (2, 2, 1)$ ; $(3, 1, 1)$ has column heights $3, 1, 1$ and is self-conjugate; $(3, 1)$ transposes to $(2, 1, 1)$ and $(2, 2)$ to itself, matching the listed pairs, and taking column heights twice returns the original partition as in [F1].

1.3

For $n = 5$ , each listed consecutive pair is comparable, by the prefix sums of the two partitions: $(5) ⊳ (4, 1)$ since $5 > 4$ ; $(4, 1) ⊳ (3, 2)$ since $4 > 3$ ; $(3, 2) ⊳ (3, 1, 1)$ since $3 = 3$ and $5 > 4$ ; $(3, 1, 1) ⊳ (2, 2, 1)$ since $3 > 2$ ; $(2, 2, 1) ⊳ (2, 1, 1, 1)$ since $2 = 2$ , $4 > 3$ ; and $(2, 1, 1, 1) ⊳ (1, 1, 1, 1, 1)$ since $2 > 1$ .

1.4

The same computation for $n = 4$ gives the chain $(4) ⊳ (3, 1) ⊳ (2, 2) ⊳ (2, 1, 1) ⊳ (1, 1, 1, 1)$ : the prefix sums compare as $4 > 3$ ; then $3 > 2$ ; then $2 = 2$ and $4 > 3$ ; then $2 > 1$ , while the partitions of $n \leq 3$ form the chains $(3) ⊳ (2, 1) ⊳ (1, 1, 1)$ , $(2) ⊳ (1, 1)$ and the single partitions of $n \leq 1$ .

1.5

At $n = 6$ the partition $(4, 1, 1)$ has prefix sums $4, 5, 6$ and $(3, 3)$ has prefix sums $3, 6, 6$ , so $4 > 3$ rules out $(3, 3) ⊵ (4, 1, 1)$ while $5 < 6$ rules out $(4, 1, 1) ⊵ (3, 3)$ : the two are incomparable, and taking conjugates gives $(4, 1, 1)^{'} = (3, 1, 1, 1)$ and $(3, 3)^{'} = (2, 2, 2)$ , whose prefix sums $3, 4, 5, 6$ and $2, 4, 6, 6$ also cross, as [F3] requires.

givenF1F2F3

2.1

Steps 1.3 and 1.4 exhibit a chain through all partitions of each $n \leq 5$ , so any two partitions of the same $n \leq 5$ are comparable by transitivity of the partial order $⊵$ ; together with step 1.5, which exhibits an incomparable pair of partitions of $6$ , dominance is total exactly through size five and the first incomparable pair occurs at $n = 6$ . ∎

step 1.3step 1.4step 1.5F2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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

David Craven, Groups, Geometries and Representation Theory - Definitions 1.18-1.19 and Lemma 1.21, printed pp. 15-16 (PDF pp. 17-18) (standard reference, not scraped)
Charlotte Chan, Representation Theory of Symmetric Groups - Definition 2.12 and Remark 2.13, printed p. 9 (PDF p. 10) (standard reference, not scraped)