Exercise PLAN-408

Separable states are infinitely extendible via index-shared copies on each B_j, and k-extendibility descends to all k' <= k by discarding systems, yielding the monogamy inclusion chain Ext_1 superset ... superset SEP.

1. A separable state admits a k-extension by copying sigma_B on each B_j under a shared index.
2. The A B_j marginal recovers rho_AB via unit trace of the discarded factors.
3. Discarding systems reduces a k-extension to a k'-extension, giving the inclusion chain.

(a) Let rho_AB = sum_i p_i sigma_A^{(i)} tensor sigma_B^{(i)} be separable, with p_i >= 0 summing to 1 and the sigma^{(i)} states. Define, for any k, the state rho_{A B_1 ... B_k} := sum_i p_i sigma_A^{(i)} tensor sigma_{B_1}^{(i)} tensor ... tensor sigma_{B_k}^{(i)}, i.e. put an independent copy of sigma_B^{(i)} on each B_j, all conditioned on the same classical index i. This is a valid state (a convex combination of product states, hence positive with unit trace). Its marginal on A B_j is obtained by tracing out all B_l with l != j: tr_{B_l, l != j} gives sum_i p_i sigma_A^{(i)} tensor sigma_{B_j}^{(i)}, since each traced copy contributes tr(sigma_B^{(i)}) = 1; this equals rho_AB for every j because the expression is symmetric in the B-labels. Thus rho_AB is k-extendible for every k, i.e. infinitely extendible. (b) If rho_AB is k-extendible with extension rho_{A B_1 ... B_k}, then for any k' <= k simply trace out the last k - k' systems B_{k'+1}, ..., B_k. The reduced state rho_{A B_1 ... B_{k'}} is a valid state, and for each j <= k' its marginal on A B_j is unchanged, because tracing out additional B-systems commutes with taking the A B_j marginal; hence it is a k'-extension. Therefore k-extendibility implies k'-extendibility. Combining (a) and (b), the sets Ext_k(A:B) satisfy Ext_1 superset Ext_2 superset ... superset Ext_infinity, with Ext_1 all states and Ext_infinity containing SEP by (a). Monogamy: because a k-extension forces A to be correlated in the same way with k copies of B, a strongly entangled state (in particular a pure entangled one) admits no large extension, so moving down the chain squeezes states toward separability -- entanglement cannot be shared with arbitrarily many parties.

1. Writes the explicit k-extension of a separable state by tensoring independent copies of sigma_B^{(i)} on each B_j under the shared index i (1 weight)
2. Checks the A B_j marginal equals rho_AB using tr(sigma_B^{(i)}) = 1 and symmetry in the B-labels (1 weight)
3. Proves k-extendible implies k'-extendible by discarding k - k' systems and noting the marginals are preserved (1 weight)
4. Assembles the inclusion chain Ext_1 superset ... superset Ext_infinity containing SEP and interprets it as monogamy/obstruction to entanglement (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: 2fdc9618506c9da7e2a39ffd8f195606fc4108f5762d2b1603557deaaa68da2d

Item digest: 682c79e81015ae2267b8ddef78c927dc7e1d68ec526c14ae7e30f002b5c310c8

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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