Exercise PLAN-414

Compact normalized left Haar supplies right invariance for W=UV and hence channel covariance. Schur's scalar conclusion applies to the symmetric compression of an invariant-input output, not arbitrary outputs or the channel as a whole.

1. Expanding a rotated input groups its inside factors as (UV)_N X ((UV)^dagger)_N.
2. Uniqueness of normalized compact left Haar implies right invariance, validating W=UV with U=W V^dagger.
3. The outside V factors give covariance; at the invariant input tau_N its symmetric output block is scalar, whereas arbitrary inputs and other multiplicities need not be.

Put U_r=U^{tensor r}, and take normalized left Haar measure mu on the compact group U(d). First justify the translation actually needed. For fixed V, the right-translated measure nu(A)=mu(A V^{-1}) is a probability measure and satisfies nu(gA)=mu(g A V^{-1})=mu(A V^{-1})=nu(A). Uniqueness of normalized left Haar therefore gives nu=mu. Thus normalized compact left Haar is also right invariant. The substitution W=UV below is RIGHT translation, derived from left invariance plus normalization/uniqueness; it is not directly a left translation.

For any operator X, expand Tbar(V_N X V_N^dagger) = integral dU (U^dagger)_M T((UV)_N X ((UV)^dagger)_N) U_M. Set W=UV, so U=W V^dagger and U^dagger=V W^dagger. Right invariance just established leaves dU=dW. Consequently this equals integral dW V_M (W^dagger)_M T(W_N X (W^dagger)_N) W_M (V^dagger)_M = V_M Tbar(X) (V^dagger)_M. This proves the specified covariance, for every X, not merely density operators or symmetric inputs. Every integrand map is a unitary conjugation before and after T; positivity of every matrix amplification and trace preservation survive finite-dimensional averaging, so Tbar is again a quantum channel.

The requested one-sentence Schur-Weyl explanation is: covariance converts invariance of an INPUT into invariance of its OUTPUT, so the multiplicity-one irreducible symmetric output block is scalar by Schur's lemma, without asserting that an arbitrary input has a scalar output.

More explicitly, write Pi_r for the projector onto Sym^r(C^d) and q_d(r)=dim Sym^r(C^d). Whenever q_d(N)>0, tau_N=Pi_N/q_d(N) is an invariant density operator. Covariance implies Y=Tbar(tau_N) commutes with every V_M. The compression Pi_M Y Pi_M also commutes with the irreducible U(d) action on Sym^M. Thus, if q_d(M)>0, Pi_M Y Pi_M = (lambda/q_d(M)) Pi_M, lambda=tr(Pi_M Y), 0<=lambda<=1. This is the statement used in the source's cloning argument. It describes only that compressed block, not all of Y or a channel determined by one parameter. Nor does unitary commutation force scalars on every isotypic component: in the Schur-Weyl order V_lambda tensor U_lambda^d it permits End(V_lambda) tensor I on the multiplicity factor. Additional permutation commutation is a different condition.

For a direct boundary witness, d=2,N=M=1,T=identity gives Tbar=identity and Tbar(|0><0|)=|0><0|, not a scalar on Sym^1(C^2)=C^2. Covariance is an intertwining identity for a SUPEROPERATOR, not permission to apply the ordinary irreducible-endomorphism version of Schur directly to that superoperator.

N,M may be zero, with tensor power zero the one-dimensional tensor unit and U_0=1; the same proof applies. For d=1 the nonzero spaces and symmetric blocks are one-dimensional. For d=0 the covariance algebra still makes sense whenever such a channel exists, but positive tensor powers of C^0 are zero spaces with no trace-one state: tau_r and division by q_0(r)=0 must not be used there. For r=0 the tensor unit and its projector have dimension one. These cases do not enlarge the scalar conclusion. No optimal-cloning fidelity or efficient implementation is proved by this covariance identity alone.

1. Expands the rotated input, groups U_N V_N=(UV)_N, and keeps input/output tensor powers and adjoints in the displayed order. (1 weight)
2. Correctly identifies W=UV as right translation and derives its measure invariance from uniqueness/normalization of compact left Haar; uses U=W V^dagger and U^dagger=V W^dagger without the original inverse-substitution typo. (1 weight)
3. Pulls the fixed V_M and (V^dagger)_M outside the integral, recognizes Tbar(X), and proves covariance for every X. Does not add symmetric-input or scalar-output premises to that identity. (1 weight)
4. Gives a qualified Schur-Weyl explanation: invariant input yields invariant output, whose irreducible symmetric compression is scalar when the normalized objects exist. Does not infer scalarity for arbitrary input, for multiplicity factors, or for the entire channel. The invariant tau_N calculation, identity-channel witness and zero-normalization discussion in the reference elaborate this boundary; they are not additional premises for the covariance equation. (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: 978355f5a0bd94ec866217b30d86c71d7567df66b79cc556a0b81d5d596a73f7

Item digest: 752a79aa877ed168dd52cc60b3828093ab27d127c04242a326ecbe936e29dc7c

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "predecessor_item_digest": "7655ddef61c1ba6c3690219bfc2fe0d1480ae1f152b262040ab453308f3159d0", "predecessor_key": "qcb-core-plan-414-twirled-channel-covariance-haar", "repair_record": "shared/repairs/plan-414-invariant-output-block-repair.json", "repair_record_digest": "4ebee5ff0c5ce67a2f1cf5ec3b53ceacafc6aaec41a99ce501937dcc8ed4d184", "review_record": "reports/textbook-v1/repairs/plan-414-invariant-output-block-repair-review.json", "review_digest": "e0260d51e579beb45173a44551f82f643fa82f8e60f0684ac836956d13f8b35b" }