Spin-1 tensor spin-K/2 precession separable bound

Abstract

The spin-1 tensor spin-K/2 precession protocol has separable bound ½ [1 + 2^{−(K−1)} binom(K−1, (K−1)/2) (K−1)/(K+1)] for every odd K ≥ 7. This is Conjecture 2, Eq. (32), of Huynh-Vu, Zaw and Scarani (arXiv:2311.00806v2).

Definition 1.1 (Spin raising matrix).

$$\forall n\in \mathbb{N},\mathrm{Jplus}\left(n\right)=(i:\mathrm{Fin}\left((n+1)\right))\mapsto (r:\mathrm{Fin}\left((n+1)\right))\mapsto \mathrm{if}\left(\mathrm{val}\left(i\right)+1=\mathrm{val}\left(r\right),\mathrm{ofReal}\left(Real.sqrt\left(\frac{\mathrm{NatCast}\left(n\right)}{2}\cdot (\frac{\mathrm{NatCast}\left(n\right)}{2}+1)-(\frac{\mathrm{NatCast}\left(n\right)}{2}-\mathrm{NatCast}\left(\mathrm{val}\left(r\right)\right))\cdot (\frac{\mathrm{NatCast}\left(n\right)}{2}-\mathrm{NatCast}\left(\mathrm{val}\left(r\right)\right)+1)\right)\right),0\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jplus (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

In the standard descending |j,m⟩ basis the raising matrix has entry √(j(j+1)−m(m+1)) on the one-step superdiagonal, with j = n/2, m = j−r and ℏ = 1.

Definition 1.2 (Spin x matrix).

$$\forall n\in \mathbb{N},\mathrm{Jx}\left(n\right)=\mathrm{smul}\left((\frac{1}{2}:\mathbb{C}),(\mathrm{Jplus}\left(n\right)+\mathrm{conjTranspose}\left(\mathrm{Jplus}\left(n\right)\right))\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jx (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

Jx is the Hermitian half-sum of the raising matrix and its conjugate transpose.

Definition 1.3 (Spin y matrix).

$$\forall n\in \mathbb{N},\mathrm{Jy}\left(n\right)=\mathrm{smul}\left((\frac{1}{2\cdot I}:\mathbb{C}),(\mathrm{Jplus}\left(n\right)-\mathrm{conjTranspose}\left(\mathrm{Jplus}\left(n\right)\right))\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jy (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

Jy is the Hermitian y component obtained from the raising matrix and its conjugate transpose.

Definition 1.4 (Spin z matrix).

$$\forall n\in \mathbb{N},\mathrm{Jz}\left(n\right)=\mathrm{diagonal}\left((i:\mathrm{Fin}\left((n+1)\right))\mapsto \mathrm{ofReal}\left(\frac{\mathrm{NatCast}\left(n\right)}{2}-\mathrm{NatCast}\left(\mathrm{val}\left(i\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jz (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

Jz is diagonal in the standard basis with entries n/2 minus the descending index.

Definition 1.5 (Spin z rotation).

$$\forall n\in \mathbb{N},\forall angle\in \mathbb{R},\mathrm{rotation}\left(n,angle\right)=Matrix.diagonal\left((i:\mathrm{Fin}\left((n+1)\right))\mapsto Complex.exp\left(-Complex.I\cdot (angle:\mathbb{C})\cdot ((\frac{(n:\mathbb{R})}{2}-(\mathrm{val}\left(i\right):\mathbb{R}):\mathbb{R}):\mathbb{C})\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.rotation (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

The diagonal spin rotation has phase exp(-I angle (n/2-i.val)) in the descending spin basis.

Definition 1.6 (Total angular momentum).

$$\forall K\in \mathbb{N},\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left((2+1)\right),\mathrm{Fin}\left((2+1)\right),\mathbb{C}\right),\forall B\in \mathrm{Matrix}\left(\mathrm{Fin}\left((K+1)\right),\mathrm{Fin}\left((K+1)\right),\mathbb{C}\right),\mathrm{total}\left(K,A,B\right)=\mathrm{kronecker}\left(A,(1:\mathrm{Matrix}\left(\mathrm{Fin}\left((K+1)\right),\mathrm{Fin}\left((K+1)\right),\mathbb{C}\right))\right)+\mathrm{kronecker}\left((1:\mathrm{Matrix}\left(\mathrm{Fin}\left((2+1)\right),\mathrm{Fin}\left((2+1)\right),\mathbb{C}\right)),B\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.total (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

The total operator is J on the tensor product, J^(1) ⊗ I + I ⊗ J^(K/2), represented by the Kronecker sum.

Definition 1.7 (Precession angle).

$$\forall K\in \mathbb{N},\forall k\in \mathrm{Fin}\left(K\right),\mathrm{theta}\left(K,k\right)=\frac{2\cdot Real.pi\cdot \mathrm{NatCast}\left(\mathrm{val}\left(k\right)\right)}{\mathrm{NatCast}\left(K\right)}$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.theta (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

The k-th protocol angle is 2πk/K for k in Fin K. NatCast is the natural-to-real cast; ofReal is the real-to-complex cast. val is the underlying natural index, and n is twice the spin.

Definition 1.8 (Precessed observable).

$$\forall K\in \mathbb{N},\forall k\in \mathrm{Fin}\left(K\right),\mathrm{Jk}\left(K,k\right)=\mathrm{smul}\left(\mathrm{ofReal}\left(Real.cos\left(\mathrm{theta}\left(K,k\right)\right)\right),\mathrm{total}\left(K,\mathrm{Jx}\left(2\right),\mathrm{Jx}\left(K\right)\right)\right)+\mathrm{smul}\left(\mathrm{ofReal}\left(Real.sin\left(\mathrm{theta}\left(K,k\right)\right)\right),\mathrm{total}\left(K,\mathrm{Jy}\left(2\right),\mathrm{Jy}\left(K\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jk (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

The protocol uses J_k = cos(2πk/K)J_x + sin(2πk/K)J_y.

Definition 1.9 (Positive spectral weight).

$$\forall x\in \mathbb{R},\mathrm{positiveWeight}\left(x\right)=\mathrm{if}\left(0<x,1,\mathrm{if}\left(x=0,\frac{1}{2},0\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.positiveWeight (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

The positive projector weights positive eigenvalues by one, zero by one half, and negative eigenvalues by zero.

Definition 1.10 (Positive spectral projector).

$$\forall T\in Type,[\mathrm{Fintype}\left(T\right)][\mathrm{DecidableEq}\left(T\right)]\forall H\in \mathrm{Matrix}\left(T,T,\mathbb{C}\right),\forall h\in \mathrm{IsHermitian}\left(H\right),\mathrm{pos}\left(h\right)=h.cfc\left(positiveWeight\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.pos (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

For a Hermitian J, pos(J) = Σ_{λ>0} P_λ(J) + ½ P_0(J), with the source’s half weight at zero. The definition requires a proof h of Hermiticity and is exactly h.cfc positiveWeight. The finite spectrum requires no continuity hypothesis; its spectral expression is U diag(positiveWeight(eigenvalues)) Uᴴ. All protocol observables are Hermitian.

Definition 1.11 (Protocol average).

$$\forall K\in \mathbb{N},Q\left(K\right)=\mathrm{smul}\left((\frac{1}{(K:\mathbb{C})}:\mathbb{C}),\sum _{k:\mathrm{Fin}\left(K\right)}\mathrm{pos}\left(\mathrm{Jk}\left(K,k\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Q (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

Q_K is the average of the positive spectral projectors over k in Fin K.

Definition 1.12 (Product vector).

$$\forall K\in \mathbb{N},\forall a\in \mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left((2+1)\right)\right),\forall b\in \mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left((K+1)\right)\right),\mathrm{productVector}\left(K,a,b\right)=WithLp.toLp\left(2,(i:\mathrm{Prod}\left(\mathrm{Fin}\left((2+1)\right),\mathrm{Fin}\left((K+1)\right)\right))\mapsto a\left(\mathrm{fst}\left(i\right)\right)\cdot b\left(\mathrm{snd}\left(i\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.productVector (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

The tensor product of a spin-1 vector and a spin-K/2 vector is represented in the product basis by pointwise multiplication of the two coordinates.

Definition 1.13 (Separable score set).

$$\forall K\in \mathbb{N},\mathrm{scores}\left(K\right)=\{t:\mathbb{R}\mid \exists a\in \mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left((2+1)\right)\right),\exists b\in \mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left((K+1)\right)\right),(\Vert a\Vert =1)\wedge \left((\Vert b\Vert =1)\wedge (t=\mathrm{re}\left((\mathrm{dotProduct}\left(\mathrm{star}\left((\mathrm{productVector}\left(K,a,b\right)).ofLp\right),\mathrm{mulVec}\left(Q\left(K\right),(\mathrm{productVector}\left(K,a,b\right)).ofLp\right)\right))\right))\right)\}$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.scores (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

The score set consists of real quadratic expectations on unit product vectors in ℂ³ ⊗ ℂ^(K+1).

Definition 1.14 (Central binomial coefficient).

$$\forall K\in \mathbb{N},c\left(K\right)=\frac{1}{2^{(K-1)}}\mathrm{NatCast}\left(Nat.choose\left((K-1),Nat.div\left((K-1),2\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.c (✓ std3).

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

c K is 2^{−(K−1)} times the central binomial coefficient. Both K−1 and Nat.div use natural arithmetic (Nat.div is floor division); NatCast casts the binomial coefficient into ℝ.

Definition 1.15 (Huynh-Vu–Zaw–Scarani Conjecture 2).

$$claim\iff (\forall K\in \mathbb{N},\mathrm{Odd}\left(K\right)\Rightarrow \left(K\ge 7\Rightarrow \mathrm{IsGreatest}\left(\mathrm{scores}\left(K\right),\frac{1}{2}(1+c\left(K\right)\frac{\mathrm{NatCast}\left((K-1)\right)}{\mathrm{NatCast}\left((K+1)\right)})\right)\right))$$

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

Citation. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

The source states: “The separable bound for {ȷ̃, ȷ̃′} = {1, K/2} with K ≥ 7 is Psep_K({1, K/2}) = ½ [1 + 2^{−(K−1)} binom(K−1, (K−1)/2) (K−1)/(K+1)].” The source defines the precession protocol by “Jk := e^{−i(2πk/K)Jz/ℏ} Jx e^{i(2πk/K)Jz/ℏ} = cos(2πk/K)Jx + sin(2πk/K)Jy, where k ∈ {0, 1, . . . , K − 1}.” Equations (2)–(3) state “PK := (1/K) Σ_{k=0}^{K−1} [Pr(Jk > 0) + ½ Pr(Jk = 0)], QK := (1/K) Σ_k pos(Jk),” and “Here, pos(Jk) is defined on the eigenstates |j, m⟩k of Jk, such that Jk|j, m⟩k = ℏm|j, m⟩k and 2 pos(Jk)|j, m⟩k = [1+sgn(m)]|j, m⟩k, with the usual convention sgn(0) = 0.” Conjecture 2 and Eq. (32) are in arXiv v2, §III, PDF p. 8; Eqs. (1)–(3) are on PDF p. 2. The Lean statement binds the natural indices, casts them into ℝ for the final expression, and uses natural-number division in c.

Theorem 1.16 (Proof of the separable bound).

$$claim$$

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

Resolves. Problems/huynh-vu-zaw-scarani-2023-precession-separable-bound (proved) by D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.result.

Source. Repository-derived.

Acknowledgement. Khoi-Nguyen Huynh-Vu; Lin Htoo Zaw; Valerio Scarani (2024). Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum. URL: https://arxiv.org/abs/2311.00806.

Commentary.

The proof diagonalizes the spin-K/2 Jx operator with the binomial eigenbasis, evaluates the rotation average by the K-th root-of-unity filter, decomposes the half-integer sign spectrum, and compresses the product quadratic form to a six-index off-diagonal block. The squared Frobenius estimate is convex in |a₁|² for K ≥ 7 and is attained by the spin-1 middle state and an endpoint singular vector.

References

• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jk
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jplus
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jx
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jy
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Jz
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.Q
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.c
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.claim
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.pos
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.positiveWeight
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.productVector
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.result
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.rotation
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.scores
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.theta
• Truth anchor: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound.total