ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Hook lengths for one-row, one-column and hook shapes

Example

For $n \geq 1$ , under the hook length formula: (i) for $λ = (n)$ the hooks are $h (1, j) = n - j + 1$ ( $1 \leq j \leq n$ ), the product is $n!$ , and $f^{(n)} = 1$ ; (ii) for $λ = (1^{n})$ the hooks are again $1, 2, \dots, n$ , the product is $n!$ , and $f^{(1^{n})} = 1$ ; (iii) for $n \geq 2$ and $λ = (n - 1, 1)$ the hooks are $h (1, 1) = n$ , $h (1, j) = n - j$ for $2 \leq j \leq n - 1$ , and $h (2, 1) = 1$ , so the product is $n (n - 2)!$ and $f^{(n - 1, 1)} = n! / (n (n - 2)!) = n - 1$ . For $n = 1$ the shape $(0, 1)$ is not a partition; the smallest member of this hook-shape family is $(1, 1)$ for $n = 2$ , where $f^{(1, 1)} = 1$ agrees with $n - 1 = 1$ computed in the one-column case.

Facts & Assumptions

Given: Integers $n \geq 1$ and the partitions $(n)$ , $(1^{n})$ and, for $n \geq 2$ , $(n - 1, 1)$ of $n$ , with their Young diagrams and conjugates.

[F1]

$h (i, j) = λ_{i} - j + λ_{j}^{'} - i + 1$ for $(i, j) \in [λ]$ and $P (λ) = \prod h$ ; in particular $h (1, j) = λ_{1} - j + λ_{j}^{'}$ and $h (i, 1) = λ_{i} - 1 + λ_{1}^{'} - i + 1$ (Hook, arm, leg, and hook length of a box).

[F2]

$f^{λ} = n! / P (λ)$ for $λ ⊢ n \geq 1$ , so $f^{λ}$ is determined by the multiset of hook lengths (The hook length formula).

Verification

technique · direct

1.1F1F2algebra

(One row.) For $λ = (n)$ one has $λ_{j}^{'} = 1$ for $1 \leq j \leq n$ , so $h (1, j) = n - j + 1 - 1 + 1 = n - j + 1$ , the hooks are $n, n - 1, \dots, 1$ , the product is $n!$ , and [F2] gives $f^{(n)} = n! / n! = 1$ ; this includes $n = 1$ with the single hook $h (1, 1) = 1$ .

1.2F1F2algebra

(One column.) For $λ = (1^{n})$ one has $λ_{1}^{'} = n$ and $λ_{j}^{'} = 0$ for $j \geq 2$ , so $h (i, 1) = 1 - 1 + n - i + 1 = n - i + 1$ for $1 \leq i \leq n$ and there are no other boxes; the hooks are again $n, n - 1, \dots, 1$ , the product is $n!$ , and [F2] gives $f^{(1^{n})} = 1$ .

1.3F1givenalgebra

(Hook shape, $n \geq 3$ .) For $λ = (n - 1, 1)$ the conjugate is $λ^{'} = (2, 1, \dots, 1)$ with $λ_{1}^{'} = 2$ and $λ_{j}^{'} = 1$ for $2 \leq j \leq n - 1$ : $h (1, 1) = (n - 1) - 1 + 2 - 1 + 1 = n$ ; for $2 \leq j \leq n - 1$ , $h (1, j) = (n - 1) - j + 1 - 1 + 1 = n - j$ , giving the values $n - 2, n - 3, \dots, 1$ ; and $h (2, 1) = 1 - 1 + 2 - 2 + 1 = 1$ .

2.1F2step 1.3algebra

(Hook shape, product and count.) The product of the hooks of step 1.3 is $n \cdot (n - 2)! \cdot 1 = n (n - 2)!$ (the factors $n - 2, \dots, 1$ contribute $(n - 2)!$ ); hence [F2] gives $f^{(n - 1, 1)} = n! / (n (n - 2)!) = (n - 1)! / (n - 2)! = n - 1$ .

3.1step 1.2step 1.3step 2.1algebra

(The case $n = 2$ .) Here $(n - 1, 1) = (1, 1) = (1^{2})$ is the one-column shape of step 1.2: the formula of step 2.1 reads $n (n - 2)! = 2 \cdot 0! = 2$ , the hook product is indeed $2$ , and $f^{(1, 1)} = 1 = n - 1$ ; the intermediate range $2 \leq j \leq n - 1$ is empty and contributes the empty product $1$ .

4.1F1step 1.1step 1.2given∎

(Endpoint $n = 1$ .) The shape $(n - 1, 1) = (0, 1)$ is not a partition, so the hook-shape family begins at $n = 2$ ; for $n = 1$ the only partitions are $(1) = (1^{1})$ , covered by steps 1.1 and 1.2 with $f^{(1)} = 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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 A. Craven, Groups, Geometries and Representation Theory (Spring Term 2013 lecture notes, 42 pp.) (standard reference, not scraped)
Jeremy L. Martin, Lecture Notes on Algebraic Combinatorics (263 pp.) (standard reference, not scraped)
Charlotte Chan, Representation Theory of Symmetric Groups (Oxford Hilary Term 2011 lecture notes, 40 PDF pp.) (standard reference, not scraped)