Exact W-state Bell-measurement optimum

Abstract

The W-state Bell-measurement network optimum is sqrt(13)/3.

The three tensor factors are ordered Alice, end node, Charlie. Pauli coordinates k : Fin 3 are X, Y, Z in that order. The function pauli1 is D5.S3.Quantum.QuantumChannels.SicKFidelity.SicKFidelityPauliWeight.pauli1; its arguments 1, 2, 3 give X, Y, Z. Central indices lie in Fin 4; index 0 is the identity and indices 1, 2, 3 select the three members of the frame. Every real coefficient is embedded in the complex scalars by Complex.ofReal. The maxima are represented by sSup.

Definition 1.1 (The W-state conditional correlation vector).

$$\forall (e:\mathrm{Fin}\left(3\right)\to \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right)),(\forall (f:\mathrm{Fin}\left(3\right)\to \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right)),(\forall (\mu :\mathrm{Fin}\left(4\right)),(\forall (\nu :\mathrm{Fin}\left(4\right)),(\mathrm{tau}\left(e,f,\mu ,\nu \right)=(\lambda (k:\mathrm{Fin}\left(3\right))\mapsto \mathrm{let}(w:((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\times \mathrm{Fin}\left(2\right))\to \mathbb{C}):=(\lambda (i:((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\times \mathrm{Fin}\left(2\right)))\mapsto \mathrm{if}((i=((0,0),1))\vee ((i=((0,1),0))\vee (i=((1,0),0))))\mathrm{then}(\frac{1}{Complex.sqrt\left(3\right)}:\mathbb{C})\mathrm{else}0);Complex.re\left(Matrix.trace\left(Matrix.vecMulVec\left(w,\mathrm{star}\left(w\right)\right)\cdot Matrix.kronecker\left(Matrix.kronecker\left((\mathrm{if}(\mu =0)\mathrm{then}1\mathrm{else}\sum _{(k:\mathrm{Fin}\left(3\right))}(HSMul.hSMul\left(Complex.ofReal\left(e\left(\mathrm{if}(\mu =0)\mathrm{then}0\mathrm{else}Fin.mk\left(Nat.sub\left(\mathrm{val}\left(\mu \right),1\right),\mathrm{by}\mathrm{omega}\right),k\right)\right),pauli1\left(Fin.succ\left(k\right)\right)\right))),pauli1\left(Fin.succ\left(k\right)\right)\right),(\mathrm{if}(\nu =0)\mathrm{then}1\mathrm{else}\sum _{(k:\mathrm{Fin}\left(3\right))}(HSMul.hSMul\left(Complex.ofReal\left(f\left(\mathrm{if}(\nu =0)\mathrm{then}0\mathrm{else}Fin.mk\left(Nat.sub\left(\mathrm{val}\left(\nu \right),1\right),\mathrm{by}\mathrm{omega}\right),k\right)\right),pauli1\left(Fin.succ\left(k\right)\right)\right)))\right)\right)\right))))))$$

Formalization. D5/S3/Quantum/MeasurementGeometry/WStateBellMeasurementOptimum.tau (✓ std3).

Citation. Sudip Chakrabarty and Amit Kundu (2026). Network nonlocality with tripartite entangled sources. DOI: 10.48550/arXiv.2610.35838. URL: https://arxiv.org/abs/2610.35838v1.

Commentary.

PDF page 4 defines τμν = (Tr[ρ Aμ ⊗ σₖ ⊗ Cν])ₖ₌₁,₂,₃. It states: “We write Aᵢ = eᵢ · σ and Cⱼ = fⱼ · σ, and set A₀ = C₀ = 𝕀.” For a nonzero central index μ its frame index has natural value μ.val − 1; Nat.sub denotes truncated natural subtraction. PDF page 3 defines |W⟩ = 1/√3 (|001⟩ + |010⟩ + |100⟩). Here ρ is Matrix.vecMulVec w (star w), with the displayed literal W ket w. The real part is taken after the trace.

Definition 1.2 (Optimization over orthogonal unit directions).

$$\forall (u:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\forall (v:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\mathrm{lambda}\left(u,v\right)=\mathrm{sSup}\left(\{(q:\mathbb{R})|\exists (n:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\exists (n^{\prime }:\mathrm{Fin}\left(3\right)\to \mathbb{R}),((\sum _{(coord:\mathrm{Fin}\left(3\right))}(n{\left(coord\right)}^2)=1)\wedge ((\sum _{(coord:\mathrm{Fin}\left(3\right))}(n^{\prime }{\left(coord\right)}^2)=1)\wedge (((\sum _{(i:\mathrm{Fin}\left(3\right))}(n\left(i\right)\cdot n^{\prime }\left(i\right)))=0)\wedge (q=(\sum _{(i:\mathrm{Fin}\left(3\right))}(u\left(i\right)\cdot n\left(i\right)){)}^2+(\sum _{(i:\mathrm{Fin}\left(3\right))}(v\left(i\right)\cdot n^{\prime }\left(i\right)){)}^2)))))\}\right)))$$

Formalization. D5/S3/Quantum/MeasurementGeometry/WStateBellMeasurementOptimum.lambda (✓ std3).

Citation. Sudip Chakrabarty and Amit Kundu (2026). Network nonlocality with tripartite entangled sources. DOI: 10.48550/arXiv.2610.35838. URL: https://arxiv.org/abs/2610.35838v1.

Commentary.

PDF page 4: “The network value therefore depends on how much of τμν and τμ′ν′ two perpendicular directions can capture. For two vectors τ, τ′ this is” Λ(τ, τ′) = max over n ⟂ n′ of (τ · n)² + (τ′ · n′)². Both directions have squared Euclidean length one. Every scalar product and squared length is displayed as its three-coordinate sum.

Definition 1.3 (The exact optimum assertion).

$$\mathrm{claim}\iff (Real.sqrt\left(\mathrm{sSup}\left(\{(q:\mathbb{R})|\exists (e:\mathrm{Fin}\left(3\right)\to \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right)),(\exists (f:\mathrm{Fin}\left(3\right)\to \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right)),((\mathrm{Orthonormal}\left(\mathbb{R},e\right))\wedge ((\mathrm{Orthonormal}\left(\mathbb{R},f\right))\wedge (\exists (\mu :\mathrm{Fin}\left(4\right)),(\exists (\nu :\mathrm{Fin}\left(4\right)),(\exists ({\mu }^{\prime }:\mathrm{Fin}\left(4\right)),(\exists ({\nu }^{\prime }:\mathrm{Fin}\left(4\right)),(q=\mathrm{lambda}\left(\mathrm{tau}\left(e,f,\mu ,\nu \right),\mathrm{tau}\left(e,f,{\mu }^{\prime },{\nu }^{\prime }\right)\right)))))))))\}\right)\right)=\frac{Real.sqrt\left(13\right)}{3})$$

Formalization. D5/S3/Quantum/MeasurementGeometry/WStateBellMeasurementOptimum.claim (✓ std3).

Citation. Sudip Chakrabarty and Amit Kundu (2026). Network nonlocality with tripartite entangled sources. DOI: 10.48550/arXiv.2610.35838. URL: https://arxiv.org/abs/2610.35838v1.

Commentary.

PDF page 5: “For the W state, τ₃₃ = −ẑ and τ₁₃ = ⅔x̂ are orthogonal, which gives N_c ≥ √13/3 ≈ 1.202. The numerical optimization over frames finds no larger value.” Proposition 1 on PDF page 4 maximizes Λ over both orthonormal frames and all four central indices. The assertion below includes index 0 and repeated index pairs; it concerns Bell-state measurements.

Theorem 1.4 (The exact Bell-state-measurement optimum).

$$Real.sqrt\left(\mathrm{sSup}\left(\{(q:\mathbb{R})|\exists (e:\mathrm{Fin}\left(3\right)\to \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right)),(\exists (f:\mathrm{Fin}\left(3\right)\to \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right)),((\mathrm{Orthonormal}\left(\mathbb{R},e\right))\wedge ((\mathrm{Orthonormal}\left(\mathbb{R},f\right))\wedge (\exists (\mu :\mathrm{Fin}\left(4\right)),(\exists (\nu :\mathrm{Fin}\left(4\right)),(\exists ({\mu }^{\prime }:\mathrm{Fin}\left(4\right)),(\exists ({\nu }^{\prime }:\mathrm{Fin}\left(4\right)),(q=\mathrm{lambda}\left(\mathrm{tau}\left(e,f,\mu ,\nu \right),\mathrm{tau}\left(e,f,{\mu }^{\prime },{\nu }^{\prime }\right)\right)))))))))\}\right)\right)=\frac{Real.sqrt\left(13\right)}{3}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/MeasurementGeometry/WStateBellMeasurementOptimum.result (✓ std3). ∎

Resolves. Problems/w-state-bsm-optimum (proved) by D5/S3/Quantum/MeasurementGeometry/WStateBellMeasurementOptimum.result.

Source. Repository-derived.

Acknowledgement. Sudip Chakrabarty and Amit Kundu (2026). Network nonlocality with tripartite entangled sources. DOI: 10.48550/arXiv.2610.35838. URL: https://arxiv.org/abs/2610.35838v1.

Commentary.

For unit a and c the W correlation T(a,c) satisfies 9‖T(a,c)‖² = (2a₀c₀ + 2a₁c₁ − a₂c₂)² + 4a₂² + 4c₂². Parseval’s equality for each complete orthonormal frame bounds the selected pairs by 13/9. Identity indices give a squared length at most 4/9; identical nonidentity pairs satisfy Bessel’s bound. The standard frames give τ₃₃ = −ẑ and τ₁₃ = (2/3)x̂, which are orthogonal and attain 13/9. Taking the nonnegative square root gives √13/3. This statement does not optimize over the larger product-projective class.

References

• Truth anchor: D5/S3/Quantum/MeasurementGeometry/WStateBellMeasurementOptimum.claim
• Truth anchor: D5/S3/Quantum/MeasurementGeometry/WStateBellMeasurementOptimum.lambda
• Truth anchor: D5/S3/Quantum/MeasurementGeometry/WStateBellMeasurementOptimum.result
• Truth anchor: D5/S3/Quantum/MeasurementGeometry/WStateBellMeasurementOptimum.tau
• Dependency: D5/S3/Quantum/Contextuality/EightVertexQutritBound
• Dependency: D5/S3/Quantum/FiniteDimensional
• Dependency: D5/S3/Quantum/QuantumChannels/HiaiRuskaiRiemannianContraction
• Dependency: D5/S3/Quantum/QuantumChannels/SicKFidelity/SicKFidelityPauliWeight