Tensor Symmetry
Exercise PLAN-312
primary source nl only. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- lambda = (4,2,1) is a partition of seven.
- The hook length of a box counts boxes to its right in its row, boxes below it in its column, and the box itself.
Question
The number of standard Young tableaux of a shape lambda with n boxes equals n factorial divided by the product of all hook lengths of the diagram. Compute this number for the shape (4,2,1), displaying the hook length of every box, and separately compute the number for the single-row shape (n) and the single-column shape with n boxes to confirm the formula gives the expected extreme cases.
Hint: mathematical route
The hook length formula gives thirty-five standard tableaux for shape (4,2,1) and exactly one for a single row or single column of n boxes.
- The hook lengths of (4,2,1) are six, four, two, one; three, one; one.
- Their product is one hundred forty-four and seven factorial is five thousand forty.
- The quotient is thirty-five standard tableaux.
- Single-row and single-column shapes have hook product n factorial, giving count one.
Reference solution
For the shape (4,2,1) with seven boxes, the hook lengths are as follows. First row, four boxes: the leftmost has three boxes to its right, two boxes below it (one in each of rows two and three in that column), plus itself, giving six; the next has two to the right, one below, plus itself, giving four; the next has one to the right, none below, plus itself, giving two; the last has none to the right, none below, plus itself, giving one. Second row, two boxes: the leftmost has one to the right, one below (row three in that column), plus itself, giving three; the next has none to the right, none below, plus itself, giving one. Third row, one box: hook length one. The product of hooks is six times four times two times one times three times one times one equal to one hundred forty-four. Then seven factorial is five thousand forty, and five thousand forty divided by one hundred forty-four equals thirty-five, so there are thirty-five standard tableaux of shape (4,2,1). Extremes: for the single row (n) every hook length is just the number of boxes to its right plus itself, giving n, n minus one, down to one, whose product is n factorial, so the count is n factorial over n factorial equal to one. For the single column with n boxes the hooks are likewise n, n minus one, down to one by symmetry, product n factorial, count one. Both extremes correctly give a single standard tableau.
Assessment rubric
- Correctly assigns all seven hook lengths of (4,2,1) as six, four, two, one in the first row, three, one in the second, one in the third (1 weight)
- Computes the hook product as one hundred forty-four and seven factorial as five thousand forty (1 weight)
- Divides to obtain thirty-five standard tableaux for (4,2,1) (1 weight)
- Checks the single-row and single-column shapes both give hook product n factorial and hence exactly one standard tableau (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
- Matrix analysis (frozen curriculum anchor; see graph registry)
- Tensor networks (frozen curriculum anchor; see graph registry)
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- website/research/sources.json
leditzky-2025-repth-qit
Source SHA-256:9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae· MIT metadata only - Primary source
Contract: 8bcc052de03afe9e938d7c6d5bd8d07aa3e843be2e27e11e8af79e56230b564a
Item digest: c90a4685cd737246275c9615869fbb1cf529c906f12504a0b94d29215f79c7a9
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.