Exercise PLAN-401

The isotropic family has trace1 for all real x. At d>=2 positivity holds exactly on[0,d^2/(d^2-1)] with tight spectral endpoints; at d=1 the whole family equals I for every real x because the complementary sector is absent.

1. For every positive dimension and real x, tr rho_d(x)=1; at d=1,Phi=I and the family is constant, while d=0 cannot support the stipulated projector.
2. The orthogonal-projector decomposition has coefficients1-x+x/d^2 and x/d^2, with nonzero sectors of ranks1 and d^2-1 only when d>=2; a coefficient multiplying the zero complementary projector imposes no positivity constraint at d=1.
3. For d>=2 the two actual sectors give the sharp interval and explicit negative witnesses outside it. For d=1 the allowed set is all R, refuting the predecessor's universal finite-endpoint assertion.

The predecessor's universal finite-interval assertion is false/inapplicable at d=1: the denominator d^2-1 then vanishes and the proposed lower constraint x>=0 is false. At d=1, Phi=I=1 on the one-dimensional joint space, so rho_1(x)=(1-x)+x=1 for EVERY real x. In particular x=-1 is still a positive trace-one state. The exact allowed set in this branch is R, not a finite interval with two tight endpoints. The label x is redundant there.

For any positive d, tr(Phi)=1 and tr(I)=d^2 give tr(rho_d(x))=1-x+(x/d^2)d^2=1 for every real x. The operator is Hermitian for real x. Write rho_d(x)=a Phi+b(I-Phi), with a=1-x+x/d^2 and b=x/d^2. These are coefficients of two orthogonal projectors, not necessarily two different numerical eigenvalues: at x=1 they coincide. For d>=2 both subspaces are nonzero, with ranks1 and d^2-1 respectively. Thus the spectrum is a with multiplicity1 and b with multiplicity d^2-1, and positivity is equivalent to a>=0 and b>=0.

Since d^2>0, b>=0 iff x>=0. Also 1-1/d^2>0 when d>=2, so a=1-x(1-1/d^2)>=0 iff x<=L_d=d^2/(d^2-1). Hence the exact allowed interval is[0,L_d]. If x<0, the unit product vector |1,2>, available for every d>=2, is orthogonal to |Phi_d> and has expectation b<0. If x>L_d, the unit vector |Phi_d> has expectation a<0. These witnesses prove necessity and sharpness, while nonnegative a,b prove sufficiency. At x=0 the state is Phi of rank1; at x=L_d it is (I-Phi)/(d^2-1), of rank d^2-1. At either endpoint the named eigenvalue is zero and becomes negative immediately outside. There is no condition x<=1: x can exceed1 up to L_d while both spectral coefficients remain nonnegative.

At d=1 the same algebraic coefficients reduce to a=1,b=x, but I-Phi=0 has rank0. Thus b is NOT an actual eigenvalue of any nonzero spectral sector, and requiring b>=0 is invalid. The sole actual eigenvalue is1, independent of x; there is no division by d^2-1 or a vanishing-eigenvalue endpoint argument. At d=0 there cannot be a rank-one trace-one projector at all: the zero-dimensional space has only the zero operator with trace0, so the premise of this family is unsatisfied. One must not define |Phi_d> or x/d^2 at d=0.

This proves the complete dimension-branch positivity statement without hiding a d>=2 standing assumption. The source Exercise6.2/Prop6.8 gives the nontrivial isotropic interval, but its parameter expression does not define the one-dimensional boundary by itself. This is an explicit change to the requested question; the historical claim is preserved for assessment, not silently accepted. No separability, partial-transpose criterion, quantum implementation or new local formal proof is inferred from positivity alone.

1. Assesses the predecessor's universal interval statement and explicitly gives d=1:Phi=I,rho(x)=I for every real x, including a negative-x witness against a universal lower bound. Does not silently add d>=2. (1 weight)
2. Proves trace1 for all real x and decomposes a Phi+b(I-Phi), giving correct nonzero-sector multiplicities for d>=2 and not treating a zero-rank sector as an eigenvalue constraint. (1 weight)
3. For d>=2 derives exactly0<=x<=d^2/(d^2-1), proves sufficiency and gives explicit unit-vector negativity witnesses outside each endpoint. (1 weight)
4. Identifies the endpoint states/ranks; handles d=1 as the full real line with no finite endpoints and d=0 as incompatible with a trace-one Phi. Makes no positivity-versus-entanglement or new formal claim. (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: f5d6e502b09f0ff671db99348e926bb515551af628bffba62aebf9a08184d1e9

Item digest: 15e38bb2abfa641ea09ccdcc12a5c39cc268fdad255f7a6ea22b182ec6192dca

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "question_version": 2, "predecessor_key": "qcb-core-plan-401-isotropic-positivity-x-range", "predecessor_item_digest": "a1e13c8ee83cf6e9502719cba3080b6fa3006bf2b81c673e32dc4ddbf412d0bd", "predecessor_contract_hash": "35796e5369f3f45d58d9b62103d321787c8fd234a7d0ed8d6b8b4c585181b9cf", "current_contract_hash": "f5d6e502b09f0ff671db99348e926bb515551af628bffba62aebf9a08184d1e9", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/plan-401-isotropic-dimension-state-successor.json", "repair_record_digest": "4918d3f5fbe8d0227ba7c73816fb923c33ed514af235ad01372127bd8c35e00d", "review_record": "reports/textbook-v1/repairs/plan-401-isotropic-dimension-state-successor-migration-revalidation-review.json", "review_digest": "7c68aef7fe677e255c275be02c6ebd7fdc251d91282413a6cf891f4e1760ed57", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }