A strict gap for the noisy GHZ witness bound

Abstract

The optimized GHZ witness bound is strictly below the geometric convex roof for three qutrits at noise three eighths.

Word (Fin d) n is the computational basis Fin n → Fin d. rankOneDensity ψ is the matrix with entries ψ(x) conjugate(ψ(y)); IsUnitState ψ means that the sum of Complex.normSq (ψ x) is one. readout A ψ is the real part of star ψ ⬝ᵥ (A *ᵥ ψ). Matrix multiplication, real scalar multiplication and finite sums have these types throughout. Nat.cast into ℝ and Complex.ofReal into ℂ display the scalar embeddings. Subtype.val displays the inclusion of a coordinate in a chosen part of a bipartition.

Definition 1.1 (The GHZ amplitude).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),((\mathrm{ghz}\left(n,d\right):(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right))\to (\mathbb{C}))=(\lambda (x:\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right))\mapsto (if(\exists (j:\mathrm{Fin}\left(d\right)),(\forall (i:\mathrm{Fin}\left(n\right)),(x\left(i\right)=j)))thenInv.inv\left((Complex.ofReal\left(Real.sqrt\left((Nat.cast\left(d\right):\mathbb{R})\right)\right):\mathbb{C})\right)else(0:\mathbb{C})))))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.ghz (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

GMEwitness.tex, line 284, defines the equal superposition of the d constant words, divided by √d. The formula gives its amplitude at every computational word and defines it for all natural n and d.

Definition 1.2 (Pure biseparability).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),(\forall (\phi :(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right))\to (\mathbb{C})),((\mathrm{IsBiseparable}\left(\phi \right))\iff ((\mathrm{IsUnitState}\left(\phi \right))\wedge (\exists (a:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)),((Finset.Nonempty\left(a\right))\wedge ((Finset.Nonempty\left(Compl.compl\left(a\right)\right))\wedge (\exists (u:((\mathrm{Subtype}\left((\lambda (i:\mathrm{Fin}\left(n\right))\mapsto (i\in a))\right))\to (\mathrm{Fin}\left(d\right)))\to (\mathbb{C})),(\exists (v:((\mathrm{Subtype}\left((\lambda (i:\mathrm{Fin}\left(n\right))\mapsto (i\in Compl.compl\left(a\right)))\right))\to (\mathrm{Fin}\left(d\right)))\to (\mathbb{C})),(\forall (x:\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right)),(\phi \left(x\right)=u\left((\lambda (i:\mathrm{Subtype}\left((\lambda (i:\mathrm{Fin}\left(n\right))\mapsto (i\in a))\right))\mapsto (x\left(Subtype.val\left(i\right)\right)))\right)\cdot v\left((\lambda (i:\mathrm{Subtype}\left((\lambda (i:\mathrm{Fin}\left(n\right))\mapsto (i\in Compl.compl\left(a\right)))\right))\mapsto (x\left(Subtype.val\left(i\right)\right)))\right))))))))))))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.IsBiseparable (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

A unit vector is biseparable when its amplitudes factor across a nonempty proper set a of parties. The two factors are arbitrary complex functions on the coordinates in a and its complement. This expresses the pure biseparable states in GMEwitness.tex, lines 284 and 307–309.

Definition 1.3 (The support projector).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),((\mathrm{supportProjector}\left(n,d\right):\mathrm{Matrix}\left(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathbb{C}\right))=Matrix.diagonal\left((\lambda (x:\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right))\mapsto (if(Finset.card\left(Finset.image\left(x,(Finset.univ:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right))\right)\right)\le (2:\mathbb{N}))then(1:\mathbb{C})else(0:\mathbb{C})))\right)))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.supportProjector (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

The diagonal entry is one exactly on words using at most two distinct symbols. These are the constant words and the distinct arrangements of two-symbol words in GMEwitness.tex, lines 690–699. The cardinality in the condition is natural-valued.

Definition 1.4 (The GHZ witness operator).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),((\mathrm{witnessOp}\left(n,d\right):\mathrm{Matrix}\left(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathbb{C}\right))=HSMul.hSMul\left(\frac{1}{(Nat.cast\left(d\right):\mathbb{R})},\mathrm{supportProjector}\left(n,d\right)\right)-\mathrm{rankOneDensity}\left(\mathrm{ghz}\left(n,d\right)\right)))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.witnessOp (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

GMEwitness.tex, lines 295–300, gives one dth of the support projector minus the GHZ rank-one matrix. The coefficient is a real scalar; the natural dimension is cast to ℝ before division.

Definition 1.5 (The noisy GHZ matrix).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),(\forall (p:\mathbb{R}),((\mathrm{noisyGhz}\left(n,d,p\right):\mathrm{Matrix}\left(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathbb{C}\right))=HSMul.hSMul\left(\frac{p}{(Nat.cast\left(d\right):\mathbb{R}{)}^n},(1:\mathrm{Matrix}\left(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathbb{C}\right))\right)+HSMul.hSMul\left(1-p,\mathrm{rankOneDensity}\left(\mathrm{ghz}\left(n,d\right)\right)\right))))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.noisyGhz (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

GMEwitness.tex, line 284, mixes white noise with the GHZ rank-one matrix. The identity has dimension dⁿ, and its coefficient is p/dⁿ. The definition accepts every real p; the probability restrictions occur in claim.

Definition 1.6 (The witness expectation).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),(\forall (p:\mathbb{R}),((\mathrm{witnessValue}\left(n,d,p\right):\mathbb{R})=Complex.re\left(Matrix.trace\left(\mathrm{noisyGhz}\left(n,d,p\right)\cdot \mathrm{witnessOp}\left(n,d\right)\right)\right))))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.witnessValue (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

GMEwitness.tex, line 301, defines the trace of the noisy GHZ matrix times the witness. The real part gives its real-valued expectation.

Definition 1.7 (The pure geometric measure).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),(\forall (\psi :(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right))\to (\mathbb{C})),((\mathrm{geometricMeasurePure}\left(\psi \right):\mathbb{R})=1-\mathrm{sSup}\left(\{(t:\mathbb{R})|\exists (\phi :(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right))\to (\mathbb{C})),((\mathrm{IsBiseparable}\left(\phi \right))\wedge (t=Complex.normSq\left(\mathrm{dotProduct}\left(\mathrm{star}\left(\phi \right),\psi \right)\right)))\}\right))))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.geometricMeasurePure (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

GMEwitness.tex, line 284, subtracts the largest squared biseparable overlap from one. Here sSup is the real supremum of the squared overlaps with all biseparable unit vectors.

Definition 1.8 (The finite-ensemble convex roof).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),(\forall (\rho :\mathrm{Matrix}\left(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right),\mathbb{C}\right)),((\mathrm{geometricMeasure}\left(\rho \right):\mathbb{R})=\mathrm{sInf}\left(\{(t:\mathbb{R})|\exists (k:\mathbb{N}),(\exists (p:(\mathrm{Fin}\left(k\right))\to (\mathbb{R})),(\exists (\psi :(\mathrm{Fin}\left(k\right))\to ((\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right))\to (\mathbb{C}))),((\forall (i:\mathrm{Fin}\left(k\right)),(0\le p\left(i\right)))\wedge ((\sum _{i:\mathrm{Fin}\left(k\right)}(p\left(i\right))=1)\wedge ((\forall (i:\mathrm{Fin}\left(k\right)),(\mathrm{IsUnitState}\left(\psi \left(i\right)\right)))\wedge ((\rho =\sum _{i:\mathrm{Fin}\left(k\right)}(HSMul.hSMul\left(p\left(i\right),\mathrm{rankOneDensity}\left(\psi \left(i\right)\right)\right)))\wedge (t=\sum _{i:\mathrm{Fin}\left(k\right)}(p\left(i\right)\cdot \mathrm{geometricMeasurePure}\left(\psi \left(i\right)\right)))))))))\}\right))))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.geometricMeasure (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

GMEwitness.tex, lines 284–288, extends the pure measure by the convex roof. The infimum here ranges over all finite ensembles: nonnegative real weights summing to one, unit pure vectors, and exact rank-one reconstruction of the matrix. The value averaged in each ensemble is the pure geometric measure.

Definition 1.9 (The convex conjugate).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),(\forall (r:\mathbb{R}),((\mathrm{hatE}\left(n,d,r\right):\mathbb{R})=\mathrm{sSup}\left(\{(t:\mathbb{R})|\exists (\psi :(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right))\to (\mathbb{C})),(\exists (\phi :(\mathrm{Word}\left(\mathrm{Fin}\left(d\right),n\right))\to (\mathbb{C})),((\mathrm{IsUnitState}\left(\psi \right))\wedge ((\mathrm{IsBiseparable}\left(\phi \right))\wedge (t=\mathrm{readout}\left(HSMul.hSMul\left(r,\mathrm{witnessOp}\left(n,d\right)\right)+\mathrm{rankOneDensity}\left(\phi \right),\psi \right)-1))))\}\right))))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.hatE (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

GMEwitness.tex, lines 305–309, takes both pure-state optimizations. The single supremum ranges over every unit ψ and every biseparable φ, of the expectation of r times the witness plus the φ rank-one matrix, minus one.

Definition 1.10 (The optimized witness bound).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),(\forall (p:\mathbb{R}),((\mathrm{epsilonO}\left(n,d,p\right):\mathbb{R})=\mathrm{sSup}\left(\{(t:\mathbb{R})|\exists (r:\mathbb{R}),(t=r\cdot \mathrm{witnessValue}\left(n,d,p\right)-\mathrm{hatE}\left(n,d,r\right))\}\right))))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.epsilonO (✓ std3).

Citation. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

GMEwitness.tex, lines 301–305, optimizes r times the measured witness value minus the conjugate over every real slope r. The real supremum expresses this optimization.

Definition 1.11 (The universal equality question).

$$(\mathrm{claim})\iff (\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),((3\le n)\to ((3\le d)\to (\forall (p:\mathbb{R}),((0\le p)\to ((p\le 1)\to (\mathrm{epsilonO}\left(n,d,p\right)=\mathrm{geometricMeasure}\left(\mathrm{noisyGhz}\left(n,d,p\right)\right)))))))))$$

Formalization. D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

GMEwitness.tex, line 325, asks whether the optimized witness bound equals the geometric measure of the noisy GHZ state. The displayed equality question quantifies over all natural n and d at least three and every real noise probability p between zero and one.

Theorem 1.12 (Three qutrits give a strict gap).

$$\neg (\mathrm{claim})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.result (✓ std3). ∎

Resolves. Problems/xu-et-al-2023-noisy-ghz-witness-bound-gap (refuted) by D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.result.

Source. Repository-derived.

Acknowledgement. Xin-Yu Xu; Qing Zhou; Shuai Zhao; Shu-Ming Hu; Li Li; Nai-Le Liu; Kai Chen (2023). General framework for genuine multipartite entanglement detection. DOI: 10.1103/PhysRevA.107.052405. URL: https://arxiv.org/abs/2211.05563v1.

Commentary.

Take n = d = 3 and p = 3/8. Write G for the GHZ rank-one projector, P for the support projector and Q = I − P. Counting the computational words gives Tr(P) = 21 and Tr(Q) = 6. The GHZ vector is unit, P² = P, PG = GP = G and G² = G. Thus P − G and Q are positive semidefinite. Consequently ρ = I/72 + (5/8)G, W = P/3 − G and Tr(ρW) = −1/3.

The unit vector (4|000⟩ + |111⟩ + |222⟩)/√18 has P expectation one, G expectation 2/3, W expectation −1/3 and squared overlap 8/9 with |000⟩. The latter vector factors across the first party and the other two parties. For every unit vector the W expectation lies between −1 and 1/3, and every squared overlap of unit vectors is at most one. These estimates bound the set defining hatE at slope r above by |r|. The chosen pair belongs to this set and gives hatE(3,3,r) ≥ −r/3 − 1/9. The set defining epsilonO is nonempty by taking r = 0; each of its values is at most 1/9, so epsilonO(3,3,3/8) ≤ 1/9.

For any biseparable φ, let g be its G expectation and s its P expectation. Choose a nonempty proper cut on which φ factors as u times v. Cauchy–Schwarz bounds the squared sum of its three constant-word amplitudes by the product of the sums of the squared constant amplitudes of u and v. This product is the sum over the nine words constant on each side of the cut. Those nine words are distinct because both parts are nonempty, and each lies in the support of P. Their nonnegative squared amplitudes therefore sum to at most s. The squared constant-word sum equals 3g, proving 3g ≤ s.

Set B = −(2/3)W + Q/9, D = (2/3)G + (4/3)(P − G) + Q and T = (3/2)G + (3/4)(P − G) + Q. The inequality 3g ≤ s and normalization give ⟨φ,Tφ⟩ = 1 + (3g − s)/4 ≤ 1. Also D = (2/3)I + (2/3)(P − G) + Q/3 is positive definite, T is positive semidefinite, and the projector identities give DT = I. Apply the positive semidefinite Cauchy–Schwarz inequality for D to ψ and Tφ. Using DTφ = φ and the Hermitian symmetry of T gives |⟨φ,ψ⟩|² ≤ ⟨φ,Tφ⟩⟨ψ,Dψ⟩ ≤ ⟨ψ,Dψ⟩. There is a biseparable vector |000⟩, so taking the supremum over biseparable overlaps is legitimate. Since D + B = (10/9)I, every unit ψ satisfies geometricMeasurePure ψ ≥ ⟨ψ,Bψ⟩ − 1/9.

The relations GQ = 0 and Tr(Q) = 6 give Tr(ρQ) = 1/12. Hence Tr(ρB) − 1/9 = −(2/3)Tr(ρW) + Tr(ρQ)/9 − 1/9 = 13/108. The matrix ρ is positive semidefinite with trace one, so a finite spectral ensemble exists. For any such ensemble, the rank-one trace identity identifies the average of ⟨ψ,Bψ⟩ with Tr(ρB). Multiplying the pure bound by each nonnegative weight and summing yields an average geometric measure at least 13/108. Taking the infimum over the nonempty set of finite ensembles gives geometricMeasure ρ ≥ 13/108. The equality in claim at these parameters would imply 13/108 ≤ 1/9 = 12/108, a contradiction. No exact value of the convex roof is asserted.

References

• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.IsBiseparable
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.claim
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.epsilonO
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.geometricMeasure
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.geometricMeasurePure
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.ghz
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.hatE
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.noisyGhz
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.result
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.supportProjector
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.witnessOp
• Truth anchor: D5/S3/Quantum/Entanglement/Witness/NoisyGhzWitnessBoundGap.witnessValue
• Dependency: D5/S3/Quantum/Divergence/CanonicalRelativeModularModel
• Dependency: D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness
• Dependency: D5/S3/Quantum/Information/MultiEntropyPositivityRefutation
• Dependency: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality
• Dependency: D5/S3/Zeros/CriticalPoints/RankOneTraceBound