Quantum Information Apps
Exercise PLAN-402
primary source nl only. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- d>=3 integer; k>=1 integer
- Werner alpha∈[-1,1]; isotropic x in its valid state range
- The supplied analytic criteria are exactly alpha>=(1-d)/k and x>=d/(d+1)*(1-1/k)
Question
Fix d>=3. A d-dimensional Werner state has parameter alpha in [-1,1] and is k-extendible exactly when alpha >= (1-d)/k. An isotropic state has valid parameter x>=0 and is k-extendible exactly when x >= [d/(d+1)](1-1/k), for positive integers k. Using these given criteria, prove every Werner state is2-extendible, determine the largest k for a fixed isotropic x below d/(d+1), and find the two parameter thresholds for extendibility at every k. Explain why the numerator grouping in (1-d)/k is essential.
Hint: mathematical route
Exact extendibility thresholds with Werner fraction(1-d)/k; all d>=3 states2extendible, finite isotropic k cutoff and allk parameter limits.
- At k2 the Werner threshold(1-d)/2<=-1, so all allowed alpha satisfy it.
- The Werner thresholds increase to0; satisfying every k is equivalent to alpha>=0.
- Rearranging the isotropic criterion below c gives the exact integer cutoff; at or above c every k works.
- Changing fraction parentheses changes the supremum from0to1 and is not the same theorem.
Reference solution
For Werner states and k=2, (1-d)/2<=-1 because d>=3. Every allowed alpha>=-1 therefore satisfies the2-extendibility criterion. The thresholds (1-d)/k increase toward0 as k grows, since1-d<0. Thus satisfying every k is equivalent to alpha>=0: if alpha<0 a sufficiently large k violates the inequality. For isotropic states write c=d/(d+1)>0. The criterion x>=c(1-1/k) is equivalent to1/k>=1-x/c. For0<=x<c this right side is positive, so precisely the integers1<=k<=1/(1-x/c) are allowed; the largest is the floor of that real bound. If x>=c, every k satisfies the inequality. Hence all-k thresholds are alpha>=0 and x>=d/(d+1). This calculation uses (1-d)/k, not1-d/k. The latter tends to1 instead of0 and gives a different, false criterion for this parameterization. These conclusions follow from the stated analytic criteria, not from a new proof of the upstream extendibility theorem.
Assessment rubric
- Use the exact grouped numerator and d>=3 to prove2extendibility (1 weight)
- Derive floor cutoff for0<=x<c and allk forx>=c (1 weight)
- Correct monotone thresholds and allk limits0,c (1 weight)
- Explain why (1-d)/k is not1-d/k (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
- Operator and semigroup theory (frozen curriculum anchor; see graph registry)
- Probability and sampling (frozen curriculum anchor; see graph registry)
- Matrix analysis (frozen curriculum anchor; see graph registry)
Lean view and evidence boundary
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.
Sources and provenance
- website/research/sources.json
leditzky-2025-repth-qit
Source SHA-256:9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae· MIT metadata only - Primary source
Contract: 69f1ec804ea09ae308d5a32cb0672e3df022e9d31fe560443b91ecbbb62d5107
Item digest: e44a4b02385956e555df305910fd11506ff3e11002d06ca0e3b57f07499a1820
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.