Exercise PLAN-307

With the source convention e_T=r_T*c_T, columns act first. More than d rows force signed column cancellation on every basis word, hence c_T=0 on the whole tensor space and the Young-image piece is absent, without commuting row and column sums.

1. Each tensor basis word fills T by recording its factor labels in the boxes carrying the corresponding position numbers.
2. The source Young symmetrizer is e_T=r_T*c_T: signed COLUMN antisymmetrization acts first on column vectors, then ROW symmetrization; the factors are not generally interchangeable.
3. If the first column has p>d boxes, pigeonhole supplies equal labels and a column transposition tau that fixes the input word and has sign-1.
4. The identity c_T*Q_tau=-c_T kills every basis word, so c_T is zero on the entire space before the row product is taken. Thus e_T=0 and its image vanishes; this proves exclusion, not nonzero action on every allowed filling.

Fix a standard tableau T of shape lambda and write Q_pi for the source's permutation action on tensor factors, so Q_pi*Q_sigma=Q_(pi*sigma). Let R_T and C_T be the subgroups permuting positions within each row and column of T. Define the row sum r_T=sum_{rho in R_T} Q_rho and the signed column sum c_T=sum_{kappa in C_T} sgn(kappa)*Q_kappa. The source convention is e_T=r_T*c_T. On column vectors this means e_T(v)=r_T(c_T(v)): COLUMN antisymmetrization acts first, then ROW symmetrization. No commutation of these two sums is assumed.

A tensor basis word v=e_{i_1} tensor ... tensor e_{i_n} fills the box carrying the number j in T with the label i_j. Suppose lambda has p>d nonempty rows. Its first column has p boxes, whose labels come from an alphabet of size d, so some two first-column positions have the same label. Let tau be their transposition. It lies in C_T, has sign-1, and fixes this basis word: Q_tau*v=v. Reindexing the entire signed column sum by kappa -> kappa*tau gives c_T*Q_tau=-c_T. Consequently c_T*v=c_T*Q_tau*v=-c_T*v. Over C,2 is invertible, so c_T*v=0.

The repeated pair may depend on the chosen basis word, but the preceding argument applies to EVERY word in the tensor basis. By linearity c_T is therefore the ZERO OPERATOR on the entire tensor power. Only after establishing this whole-space statement do we multiply by the row sum: e_T=r_T*c_T=r_T*0=0. Its image e_T((C^d) tensor n) is the zero space, so the Young-symmetrizer realization contributes no unitary-group irreducible piece of that shape. This is the precise algebraic mechanism: forced repetition in a column, a fixing transposition with negative sign, pair cancellation, and linear extension from a spanning basis. If d=0 and n>0 the tensor space is already zero; when n=0 the empty diagram has no row count exceeding a natural d, so there is no excluded case to analyze.

The earlier phrase 'row symmetrization followed by column antisymmetrization' was ambiguous: written factors r_T*c_T are not the temporal row-then-column action c_T*r_T. These products do not commute in general. For example, with T=[1,2;3] and v=e_1 tensor e_2 tensor e_1, let r=I+Q_(12) and c=I-Q_(13). Then r*c*v=0, whereas c*r*v=e_2 tensor e_1 tensor e_1-e_1 tensor e_1 tensor e_2 is nonzero. Thus one must preserve the source order, not interchange factors. In the excluded p>d regime, however, c_T has already been proved zero on the WHOLE space, so both r_T*c_T and c_T*r_T happen to vanish. That is why the old wording did not falsify the row-bound conclusion. Nothing here asserts that e_T acts nontrivially on every basis word when p<=d; absence of the forced long-column obstruction is not a pointwise survival theorem.

1. Describes the filled tableau of a tensor basis word by placing the label of factor j in T's box numbered j. (1 weight)
2. Defines row symmetrization r_T and signed column antisymmetrization c_T and states the pinned source convention e_T=r_T*c_T. Explicitly gives column-first, then row action on column vectors; does not assume r_T and c_T commute. Treats the old row-then-column wording as ambiguous rather than refuting the valid row-bound conclusion. (1 weight)
3. For p>d rows, applies pigeonhole to the first column to obtain equal labels and a column transposition tau fixing the input word with sign-1. (1 weight)
4. Uses c_T*Q_tau=-c_T to show c_T kills each basis word, then by linearity proves c_T=0 on the ENTIRE tensor space before concluding e_T=r_T*c_T=0 and the Young-image piece is absent. Does not claim every allowed p<=d filling survives. (1 weight)

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.

Read the Lean track and existing diagnostic warmups

• website/research/sources.json

  leditzky-2025-repth-qit

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: b0103ea948e0a3c59024867148d8adf149ca2cd8da13d605ee24efd98a0906c0

Item digest: 9ad464165e637fe901e26fa853df3655cd2381a13c4fd50ba68aeb231ddf7d9c

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 4. This is not measured graph distance or model difficulty.

{ "predecessor_item_digest": "5fd70ebf8a2f530a3753626e1424b902ca8e06be8d61426c16be0ec8ef234ec3", "predecessor_key": "qcb-core-plan-307-young-row-bound", "repair_record": "shared/repairs/plan-307-young-order-repair.json", "repair_record_digest": "4f130e179b86191d1b5651ee6eb1e94b6817708cd33791efe8a236d459b7e89f", "review_record": "reports/textbook-v1/repairs/plan-307-young-order-repair-migration-revalidation-review.json", "review_digest": "dc029b2911e10d0c293c83de43d48eacfcb7a9cda5da7931f24a21b145a7b35d" }