Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The ten-setting GHZ witness in odd dimensions

Abstract

The ten-setting GHZ witness bounds fidelity and genuine multipartite Schmidt dimension in every odd local dimension.

Theorem 1.1 (Finite spectral ensembles).

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.density_ensemble (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite-dimensional density matrix is a convex sum of rank-one matrices of unit vectors. The real weights are nonnegative and sum to one; Complex.ofReal displays their inclusion into the complex matrix scalars.

Theorem 1.2 (Real scaling of a quadratic form).

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.quadratic_smul (✓ std3). ∎

Source. Repository-derived.

Commentary.

The real part of a complex quadratic form scales by a real scalar r. Complex.ofReal displays the scalar used to multiply the matrix.

Theorem 1.3 (Symmetry of squared overlaps).

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.normSq_overlap_comm (✓ std3). ∎

Source. Repository-derived.

Commentary.

Exchanging two finite complex vectors conjugates their overlap and preserves its squared absolute value.

Theorem 1.4 (Squared overlap with the GHZ vector).

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.ghz_overlap_normSq (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural dimension d and every three-party complex vector v, the squared GHZ overlap is one over d times the squared absolute value of the sum of diagonal coordinates. Field division includes d = 0.

Fin d indexes coordinates from zero. Three-party coordinates use Fin d × (Fin d × Fin d). The symbols psi, rho and sigma denote the corresponding Lean vector and state variables. Complex.ofReal and Nat.cast display scalar embeddings; all divisions in Complex or Real are field divisions, while Nat.mod and Nat.sub retain natural remainder and truncated subtraction. Pi.single is the coordinate delta vector. Matrix.vecMulVec, Matrix.kroneckerMap, Matrix.mulVec, dotProduct and star have their usual Lean meanings. The density states are D5.S3.Quantum.Foundation.FiniteStateChannel.DensityState; CStarMatrix.ofMatrix.symm reads their underlying matrices. Nine labelled settings are summed with multiplicity, including when d = 1.

FormationBounds.spectral_ensemble_nonempty supplies a finite convex ensemble for each positive semidefinite trace-one coefficient matrix. Its Ensemble record stores the weights, Euclidean unit vectors and rank-one reconstruction.

Pure-state Schmidt rank is the rank of the coefficient matrix. The three-party cuts keep the other two indices in Fin d × Fin d. Supplementary V, printed page 22, uses the phase ω = exp(2πi/d), represented by WindowRegister.windowRoot.

Definition 1.5 (Quadratic-phase basis vectors).

Formalization. D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.basisVec (✓ std3).

Citation. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

Supplementary V, printed page 22, gives |e_l^(j)⟩ = d^(-1/2) Σ_m ω^(m(l+jm)) |m⟩. Here ω is exp(2πi/d), and the formula gives each coordinate.

The projector |v⟩⟨v| is PureStateHandshake.rankOneDensity v, whose entries are v_i conjugate(v_j).

Definition 1.6 (The nine product settings).

Formalization. D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.tuples (✓ std3).

Citation. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

Supplementary V, printed page 22, equation (V1), lists the nine triples in the displayed order. A List retains every label when entries coincide.

Definition 1.7 (The ten-setting operator).

Formalization. D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.witness (✓ std3).

Citation. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

Supplementary V, printed page 22: “Based on these measurements, we define the entanglement witness operator”. Equation (V2) weights the computational measurement by three and each of the nine quadratic-phase measurements by one. The modular condition is Nat.mod of the coordinate-index sum equal to zero.

Definition 1.8 (The three-party GHZ vector).

Formalization. D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.ghz (✓ std3).

Citation. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

Equation (5) specializes to the normalized sum of the coordinates (i,i,i) for three parties.

Supplementary V, printed page 22, defines W_d = tr(𝒲_d ρ). Its real expectation is GHZMeasureBiseparableBound.expect applied to the state matrix and witness operator.

The GHZ fidelity is the real matrix expectation in the normalized three-party GHZ vector, represented by RHLinalg.hermForm.

Definition 1.9 (Schmidt rank across each cut).

Formalization. D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.cutRank (✓ std3).

Citation. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

The three cuts separate party zero, one or two from the other two parties. Each Schmidt rank is the rank of the coefficient matrix with row index in Fin d and column index in Fin d × Fin d, in the displayed index order.

Definition 1.10 (Bounded Schmidt number).

Formalization. D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.SchmidtNumberLE (✓ std3).

Citation. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

A finite convex decomposition into unit vectors whose Schmidt ranks across the chosen cut are at most r defines Schmidt number at most r.

Definition 1.11 (Mixtures over the three cuts).

Formalization. D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.GMEDecomposable (✓ std3).

Citation. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

Definition 1, printed page 3: “For an arbitrary n-partite state ρ, its GME-dimension is” followed by equation (2). It minimizes over mixtures across bipartitions. Every branch has Schmidt number at most r; weights are nonnegative and sum to one.

Definition 1.12 (Genuine multipartite Schmidt dimension).

Formalization. D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.gmeDim (✓ std3).

Citation. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

Definition 1, printed page 3: “For an arbitrary n-partite state ρ, its GME-dimension is” followed by equation (2), the minimum of the admissible rank bounds. The natural infimum is attained: a spectral decomposition shows that r = d is admissible for every density state.

Definition 1.13 (The all-odd-dimensional inequalities).

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

Citation. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

Supplementary V, printed page 22, equations (V3)–(V5): “We have shown this explicitly for odd d ≤ 17 and conjecture it to hold for odd d in general.” The universal statement includes every odd natural d, every density state, both the GME-dimension bound (V3) and the fidelity bound (V4). Oddness implies d is positive. Composite dimensions and d = 1 are included.

Theorem 1.14 (Both bounds hold for every odd dimension).

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

Resolves. Problems/cobucci-tavakoli-2024-odd-ghz-ten-setting-witness (proved) by D5/S3/Quantum/Entanglement/GHZ/OddGhzTenSettingWitness.result.

Source. Repository-derived.

Acknowledgement. G. Cobucci, A. Tavakoli (2024). Detecting the dimensionality of genuine multi-particle entanglement. DOI: 10.1126/sciadv.adq4467. URL: https://arxiv.org/abs/2402.06234.

Commentary.

Additive-character orthogonality makes the operator block diagonal in the two coordinate differences. Each nonzero difference block has at most three labelled settings at a fixed frequency: oddness makes multiplication by two cancellable, and the three signed values of any nonzero difference are distinct. Cyclic Parseval then bounds these blocks by three. The zero-difference block contributes the GHZ overlap with coefficient nine and the norm with coefficient three. A spectral decomposition extends the quadratic bound to density states. The coefficient-matrix trace bound gives fidelity at most r/d for pure states of cut rank at most r, and convexity extends it to mixtures across all three cuts. Combining these estimates proves both inequalities. Mutual unbiasedness is not used. Attainment of the non-GHZ upper bound in every odd dimension and even dimensions remain open here.

References