Exercise PLAN-404

The mixed bound uses the chosen symmetric purification's d^2-dimensional local pairs and partial-trace contraction. Both displayed bounds vanish for k=o(n) at fixed d; at fixed accuracy the exact unrounded factor d compares excess n-k, not total n or rounded integer minima.

1. A specially chosen symmetric purification on A_iR_i pairs replaces the pure theorem's local dimension d by d^2; tracing references contracts the normalized trace distance and yields mixed tensor powers.
2. Strict improvement of the cap requires n-k>dk or n-k>d^2k. At accuracy epsilon the least raw-bound-certified total is k+ceil(a k/epsilon^2), a=d or d^2; only unrounded excess counts have exact factor d.
3. At fixed finite d the displayed bounds vanish iff k=o(n), while proportional retained fractions leave positive constants; varying-d bounds instead require d k/(n-k)->0 or d^2 k/(n-k)->0, with zero-copy/one-dimensional and source-domain boundaries explicit.

Use the source's trace distance D(rho,sigma)=||rho-sigma||_1/2, whose universal state-space cap is 1. Let d>=1, 0<=k<n be integers, m=n-k>0, and define the displayed numerical upper bounds B_p=sqrt(d k/m), B_m=sqrt(d^2 k/m). They compare different state classes and approximating ensembles: pure vectors in Sym^n(C^d) versus conjugation-invariant density operators on (C^d)^{tensor n}. Invariance of a density operator does not imply original-space symmetric support. When a displayed bound exceeds 1 one can still use D<=min(1,B); the question(b) asks when the DISPLAYED numerical bound strictly improves that universal cap.

(a) For a permutation-invariant rho choose matching PRODUCT bases on A^n and R^n, each R_i=C^d, and |Omega>=sum_w |w>_A|w>_R, unnormalized. The vector |Psi>=(sqrt(rho) tensor I)|Omega> has norm squared tr(rho)=1 and marginal rho. Since rho commutes with each factor permutation Q_pi, so does sqrt(rho). The real permutation matrices satisfy (Q_pi tensor Q_pi)|Omega>=|Omega>; hence the same simultaneous permutations fix |Psi>. Regroup A_1...A_n R_1...R_n into (A_1 R_1)...(A_n R_n). Thus |Psi> belongs to Sym^n(C^d tensor C^d), with LOCAL PAIR dimension d^2. Applying the pure theorem to this chosen symmetric purification replaces d by d^2, giving B_m. Tracing out R_1...R_k contracts D and sends each pure tensor power phi_AR^{tensor k} to (tr_R phi_AR)^{tensor k}, generally a mixed tensor power. Its pushforward probability measure supplies the mixed i.i.d. ensemble. The ancilla is a sufficient uniform construction, not the minimum required for every rho; an arbitrary purification need not be symmetric. No universal ancilla-resource lower bound is being asserted.

For the quantitative source route, put q_d(t)=binom(t+d-1,t). The Haar-projector identity gives conditional unnormalized k-system vectors v_phi=sqrt(q_d(m))(I tensor <phi|^{tensor m})|psi>, with p(phi)=||v_phi||^2, integral p=1, and psi_k=integral p(phi)|e_phi><e_phi|. At p=0 any normalized e_phi can be assigned without changing the integrals. Their average squared overlap with |phi>^{tensor k} equals q_d(m)/q_d(n). The exact ratio is product_{j=1}^{d-1}(m+j)/(n+j), with empty product 1. The elementary product/Bernoulli estimate bounds it below by 1-(d-1)k/(n+1), hence by 1-dk/m. Convexity of trace distance, the pure-state identity D=sqrt(1-F^2) with UNSQUARED fidelity F=|<e_phi|phi^{tensor k}>|, and Jensen give D<=sqrt(1-q_d(m)/q_d(n))<=B_p. The mixed proof uses this same route with d^2 and partial trace; it is not a statement that the original mixed rho itself lies in Sym^n(C^d).

(b) Squaring nonnegative bounds gives B_p<1 iff m>d k iff n>(1+d)k, and B_m<1 iff m>d^2 k iff n>(1+d^2)k. Equality gives the cap 1, not strict improvement. For k>0 the least integer total counts meeting these strict inequalities are (1+d)k+1 and (1+d^2)k+1, respectively.

To make the copy comparison precise, fix a retained k>0 and target normalized trace-distance tolerance 0<epsilon<1. For a=d (pure) or a=d^2 (mixed), B_a<=epsilon iff m>=a k/epsilon^2. Therefore the least integer total n CERTIFIED BY THIS RAW BOUND is n_a^{<=}=k+ceil(a k/epsilon^2). For a strict bound B_a<epsilon it is n_a^{<}=k+floor(a k/epsilon^2)+1. These certify the stated upper-bound criterion, not an optimal necessary copy complexity for the actual distance. At the real-valued thresholds it is the EXCESS m=n-k that scales by exactly d. Total thresholds satisfy n_m^*=d n_p^*-(d-1)k, and their ratio is (epsilon^2+d^2)/(epsilon^2+d), not d when d>1. Integer rounding need not preserve even the exact excess ratio. For d=2,k=1,epsilon=1/2 the least totals are 9 and 17, not 9 and 18; for epsilon^2=4/5 the least excesses are 3 and 5, not 3 and 6. At the SAME n,k>0 the two displayed errors instead obey B_m=sqrt(d) B_p. The phrase 'd-times larger total n at any fixed accuracy' is thus not an exact consequence. The real threshold ratio approaches d in the high-accuracy epsilon->0 regime at fixed d,k, but that is a qualified asymptotic statement.

(c) At any FIXED finite d>=1, as n->infinity with 0<=k(n)<n, either displayed bound vanishes exactly when k/(n-k)->0. Since k/(n-k)=[k/n]/[1-k/n], this is equivalent to k=o(n). A fixed retained k satisfies it. If k/n->c with 0<c<1, B_p->sqrt(d c/(1-c)) and B_m->sqrt(d^2 c/(1-c)); neither numerical bound vanishes. If d=d(n) varies, the exact conditions are instead d(n)k/(n-k)->0 and d(n)^2 k/(n-k)->0, respectively (equivalently d(n)k=o(n) and d(n)^2 k=o(n) for d(n)>=1). Thus k=o(n) alone is insufficient uniformly in dimension: k=1,d(n)=floor(sqrt(n)) makes the pure bound tend to zero but the mixed bound tend to 1.

Boundary and interpretation checks: k=0,n>0 gives both numerical bounds and the actual empty-marginal distance zero; within the displayed theorem domain its least allowed n is 1. At n=k, including n=k=0, the fractions are undefined and the source bound is not asserted. The zero-copy tensor unit is C and its unique normalized state is nevertheless exact; a singular bound does not itself prove impossibility of approximation. At d=1 every actual state and marginal is the unique scalar state, so the approximation is exact even where these loose numerical bounds do not vanish. At d=0 and n>0 there is no trace-one input state, not a zero-cost de Finetti problem. Epsilon=0 cannot be certified by a positive raw B at finite m when k>0, though special states and d=1 can be exactly i.i.d.; tolerances >=1 in normalized distance already follow from the universal cap. For an UNNORMALIZED trace-norm target ||rho-sigma||_1<=epsilon_1, use epsilon=epsilon_1/2, so m>=4a k/epsilon_1^2, and the universal cap is 2. These are existence/approximation guarantees from source algebra, not efficient ensemble computation, preparation circuits, gate counts or finite-bit complexity.

1. Explains the chosen permutation-invariant state's symmetric purification on n paired A_iR_i systems, with local dimension d^2 and a normalized marginal rho. Does not confuse mixed-state conjugation invariance with original symmetric support or call every purification symmetric/minimal. (1 weight)
2. Applies the pure theorem with local dimension d^2 and contracts normalized trace distance under partial trace to obtain a probability mixture of mixed tensor powers. Keeps D=||rho-sigma||_1/2 and distinguishes a sufficient ancillary construction from a resource lower bound. (1 weight)
3. Derives the strict numerical nontriviality conditions n-k>dk and n-k>d^2k (equality is not strict), interpreting them as sufficient bound thresholds, not necessary physical copy costs. Any fixed-accuracy copy comparison must distinguish total n from excess n-k and integer ceiling/floor rounding; the reference's exact formulas elaborate this distinction. (1 weight)
4. Identifies k=o(n) as precisely the fixed-finite-d numerical-bound vanishing regime, with nonzero limits at k/n->c in (0,1); if dimension varies gives the actual d(n)k/(n-k) and d(n)^2k/(n-k) criteria rather than silently holding it fixed. Does not demand or assert exactly d-times larger total n: only the unrounded excess thresholds scale by d. Handles zero-retained-copy, one-dimensional and excluded zero-denominator/state-carrier cases without mistaking loose-bound failure for an actual distance lower bound or gate-complexity theorem. (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: 6b6e41599ffc0cfa4f8e5c4c63f405cda41de360a349b07533969992adba766c

Item digest: dd6da348bd8d27c7f6c8dbcad4757906f9c2d5c65952dced139686874a3c7ee1

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "predecessor_item_digest": "4130143bb729437029128decdc18b250157a590ff27650b756eb4be353884f70", "predecessor_key": "qcb-core-plan-404-definetti-bound-scaling-dk-vs-d2k", "repair_record": "shared/repairs/plan-404-excess-copy-count-answer-repair.json", "repair_record_digest": "6d4ec330241c853e12a67ae74a436c0748647e839c4fe9f7a6bcc81a78a95e31", "review_record": "reports/textbook-v1/repairs/plan-404-excess-copy-count-answer-repair-review.json", "review_digest": "95b802b7dc8b4dd34283b8915a1173cd3312b6e9eeb2a385f9cc4bdfb6b7a746" }