Exercise PLAN-410

Applying the channel independently to each B_i of a k-extension yields a k-extension of (id tensor N)(rho_AB); CP gives positivity and TP gives both unit trace and the marginal-reduction identity.

1. Apply N independently to each B_i of a k-extension of rho.
2. Tensor products of CPTP maps are CPTP, so the output is a valid state.
3. Trace preservation lets partial trace commute past N on discarded systems, recovering sigma on each A B'_i.

Let rho_{A B_1 ... B_k} be a k-extension of rho_AB, so it is a valid state and tracing out all but B_i gives rho_{A B_i} = rho_AB for each i (identifying each B_i with B). Apply the channel N independently to each of the k B-systems: define sigma_{A B'_1 ... B'_k} := (id_A tensor N_{B_1 -> B'_1} tensor ... tensor N_{B_k -> B'_k})(rho_{A B_1 ... B_k}). This is a valid state because a tensor product of completely positive trace-preserving maps is itself completely positive and trace-preserving: complete positivity guarantees the output stays positive even in the presence of the untouched A-system and the other B-registers, and trace preservation guarantees unit trace. Now check the marginals. Fix i and trace out all B'_j with j != i. Because the maps on different systems act on independent tensor factors, the partial trace over B'_j commutes with the channels on the other systems, and for a trace-preserving map one has tr_{B'_j} N_{B_j}(X) = tr_{B_j} X. Applying this for every j != i gives tr_{B'_j, j != i} sigma_{A B'_1 ... B'_k} = (id_A tensor N_{B_i -> B'_i})( tr_{B_j, j != i} rho_{A B_1 ... B_k}) = (id_A tensor N)(rho_{A B_i}) = (id_A tensor N)(rho_AB) = sigma_{A B'}. Thus every marginal on A B'_i equals sigma_{A B'}, so sigma_{A B'_1 ... B'_k} is a k-extension of sigma_{A B'}, proving sigma is k-extendible. Complete positivity is used to ensure the constructed object is a genuine (positive) state; trace preservation is used both for its validity (unit trace) and, crucially, in the identity tr_{B'_j} N_{B_j}(X) = tr_{B_j} X that reduces the marginals on the discarded systems.

1. Starts from a k-extension of rho and applies N independently to each B_i, i.e. N^{tensor k} on the B-systems (1 weight)
2. Argues the result is a valid state because tensor products of CPTP maps are CPTP (CP for positivity, TP for unit trace) (1 weight)
3. Uses tr_{B'_j} N_{B_j}(X) = tr_{B_j} X (trace preservation) to commute partial trace past the channel on discarded systems (1 weight)
4. Verifies each A B'_i marginal equals (id tensor N)(rho_AB) = sigma, establishing the k-extension and pinpointing where CP and TP are used (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: 3776fed0bdda38b99f6cfdb6151bf365b641142ff1721aebcda479ca6f5c7e2a

Item digest: 7f9d8bb4088fa19fc4b12e3fd2430d713e777a164111aa1fed72a0972f83e30e

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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