Exercise PLAN-319

Schur-Weyl block probabilities have relative-entropy exponential rate with explicit polynomial prefactors; summing over diagrams proves total concentration in fixed neighborhoods of the spectrum, not exact matching or constant atom weights.

1. The orthogonal Schur-Weyl projections give nonnegative per-diagram weights summing to one.
2. Each weight is f_lambda times the Schur-character trace; necessary tableau-content majorization, hook/Weyl and explicit multinomial bounds control it without a pointwise survival converse.
3. The weight lies between (n+d)^(-d(d+1)/2) exp(-nD) and (n+d)^(d(d-1)/2) exp(-nD), not below the bare coefficient-one exponential; unsupported diagrams have zero weight.
4. For every fixed neighborhood of the spectrum, sum over at most(n+1)^d diagrams to bound the outside mass by a polynomial times exp(-n delta_epsilon), tending to zero. Individual blocks or exact equality are not required.

Let n>=1, let lambda=(lambda_1,...,lambda_d) be a partition of n padded by zeros, and put p=lambda/n. Write s_1>=...>=s_d>=0 for the fixed spectrum and P_lambda for the ORTHOGONAL Schur-Weyl isotypical projection. Its probability is w_lambda=tr(P_lambda*rho^tensor(n)); these weights are nonnegative and sum to1. The Schur-Weyl form rho^tensor(n)=directsum_lambda I_(V_lambda) tensor omega_lambda(rho) gives w_lambda=f_lambda*tr(omega_lambda(rho)), with f_lambda=dim(V_lambda). A general unnormalized Young symmetrizer is not substituted for this orthogonal measurement projection.

Here is a precise finite-n statement of the exponential rate, with natural logarithms. Put r=d(d-1)/2 and D(p||s)=sum_i p_i log(p_i/s_i), taking zero-p terms as0 and D=infinity if p has positive mass outside the support of s. Then (n+d)^(-r-d)*exp(-n*D(p||s)) <= w_lambda <= (n+d)^r*exp(-n*D(p||s)). Both polynomial factors matter: the coefficient-one upper inequality is false. For rho=I_2/2,n=2,lambda=(2,0), the symmetric subspace has rank3, so w_lambda=3/4, whereas exp(-nD((1,0)||(1/2,1/2)))=1/4.

For completeness the polynomial-qualified bound can be reconstructed without dropping its prefactors. First suppose s is strictly positive. The Schur character tr(omega_lambda(diag(s))) is a sum of m_lambda=dim(U_lambda^d) monomials s^nu indexed by semistandard tableaux. The row-constant tableau has weight lambda. Every tableau weight has sorted content majorized by lambda: any k labels occupy at most min(k,h) cells of each height-h column, whose sum is lambda_1+...+lambda_k. Rearranging nu against the decreasing log(s_i), then summing by parts with these partial-sum inequalities, gives s^nu<=s^lambda. Consequently s^lambda <= tr(omega_lambda(rho)) <= m_lambda*s^lambda. This uses only the necessary content restriction, not a false fixed-word survival converse.

Let C_lambda=n!/(product_i lambda_i!). Since each standard tableau is determined by which numbers occupy each increasing row, f_lambda<=C_lambda. The padded hook formula also gives f_lambda=n!*product_(i<j)(lambda_i-lambda_j+j-i)/product_i (lambda_i+d-i)! >= C_lambda/(n+d)^r: every numerator factor is at least1, and the r extra factors after the lambda_i! terms are each at most n+d. The Weyl dimension formula gives m_lambda=product_(i<j)(lambda_i-lambda_j+j-i)/(j-i)<=(n+d)^r.

The elementary multinomial bounds are (n+1)^(-d)*exp(nH(p))<=C_lambda<=exp(nH(p)), with H(p)=-sum_i p_i log p_i. One proof keeps the polynomial explicit: in n independent samples with probabilities p=lambda/n, the probability of type lambda is C_lambda*product_i p_i^lambda_i. It is at most1, giving the upper bound. It is also a maximum type probability. For another type mu, when lambda_i>0 the coordinate likelihood-ratio factor lambda_i^(mu_i-lambda_i)*lambda_i!/mu_i! is at most1: for an increase it is a product lambda_i/(lambda_i+t), and for a decrease a product (lambda_i-t)/lambda_i. If lambda_i=0 but mu_i>0, that type has probability0. Thus lambda is a mode; at most(n+1)^d types have total probability1, so its probability is at least(n+1)^(-d). This proves the lower bound, including zero entries of p with the usual0^0=1 product convention. Combining the character, hook and multinomial bounds with exp(nH(p))*s^lambda=exp(-nD(p||s)) proves the displayed lower bound, since n+1<=n+d, and proves the upper bound as well.

If s has rank q<d, a diagram with more than q rows has weight0: its first column cannot be strictly filled using only the q positive-eigenvalue labels. For such a diagram D=infinity, so both exponential bounds are0. If lambda has at most q rows, use the same character argument on the positive support; its surviving tableaux still include the leading monomial and number at most m_lambda. The same d-dependent bounds follow. No full-rank hypothesis is added. A trace-one state has d>=1; n=0 is irrelevant to normalized row lengths, which are only defined here for n>=1.

To pass from one block to concentration of the TOTAL probability, fix epsilon>0. On the probability simplex restricted to the positive support of s, D(p||s) is continuous and vanishes only at p=s. On the compact closed set ||p-s||_1>=epsilon it therefore has a strictly positive minimum delta_epsilon, unless the set is empty and the event is impossible. Diagrams outside the support already have weight0. There are at most(n+1)^d diagrams, so a union bound gives Pr(||lambda/n-s||_1>=epsilon) <= (n+1)^d*(n+d)^r*exp(-n*delta_epsilon) ->0. The count-of-diagrams factor cannot be omitted from this finite-n argument. Polynomial growth cannot defeat a fixed positive exponential rate when d is fixed.

The exact exponential scale is D: the two-sided inequalities give -log(w_lambda)/n = D(lambda/n||s)+O_d(log(n+d)/n) for nonzero supported weights. Along supported sequences with lambda/n tending to p, the rate tends to D(p||s); unsupported diagrams have zero weight and infinite rate. This is neighborhood concentration, not eventual equality lambda/n=s, and it does not say one near-spectrum block keeps a probability bounded below by a positive constant. The public question concerns mathematical probabilities, not an efficiently implemented Schur transform, a finite-bit resource certificate or a new local Lean proof.

1. Defines orthogonal Schur-Weyl block probabilities, nonnegativity and their total normalization; does not use a general unnormalized Young symmetrizer as a measurement projector. (1 weight)
2. Derives w_lambda=f_lambda tr(omega_lambda(rho)) and the polynomial-qualified exponential scale from appropriate character/dimension bounds, with natural-log entropy and zero-spectrum conventions explicit. (1 weight)
3. Retains polynomial prefactors in every finite-n claim; identifies D(lambda/n||s) as the exponential rate, not a universally valid coefficient-one upper bound. Does not assume full rank or a false content-only survival iff. (1 weight)
4. Proves concentration in every fixed neighborhood with the count-of-diagrams union factor and fixed d. Does not claim an exact matching diagram or a constant lower probability for each near-spectrum block, and distinguishes mathematical concentration from an implemented measurement/cost certificate. (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: 71f662a536110e1d7e62774362e563fe429fba9429940a16fc3410273fec0825

Item digest: 23ce008524da81fbc6003a3f740baf01af7753a835ba3a0e9657729b698f43bb

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "predecessor_item_digest": "f1c75541f386d843fd18d4f5da821e8f4752a5f188cfeef498618fbb468b386f", "predecessor_key": "qcb-core-plan-319-spectrum-concentration", "repair_record": "shared/repairs/plan-319-concentration-prefactor-repair.json", "repair_record_digest": "2fcc7f4bda646993c9b2da0b02c61c075fe06acbea9d840480a5643486142182", "review_record": "reports/textbook-v1/repairs/plan-319-concentration-prefactor-repair-migration-revalidation-review.json", "review_digest": "7b209c5dc290d3a6304d89d1276f96ba7ee0df18d30db2756cc2a5afab40be40" }