Statistical strength of the two-singlet magic square

Abstract

Four joint settings on two literal singlets beat twice CHSH under all three statistical-strength conventions.

Definition 1.1 (Uniform finite distributions).

$$\forall n\in \mathbb{N},[\mathrm{NeZero}\left(n\right)]\forall i\in \mathrm{Fin}\left(n\right),\mathrm{uniform}\left(n\right)\left(i\right)=(n:\mathrm{NNReal}{)}^{-1}$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.uniform (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Section IV.B, p. 8: “where σ° denotes the uniform distribution over the settings.” The existing Mathlib type stdSimplex NNReal (Fin n) consists of nonnegative masses summing to one. Fin n indexes n points by 0,…,n−1; [NeZero n] excludes an empty uniform law. Application uses the existing FunLike coercion of stdSimplex.

Definition 1.2 (Finite relative entropy in bits).

$$\forall alpha\in Type,[\mathrm{Fintype}\left(alpha\right)]\forall q\in alpha\to \mathrm{NNReal},\forall p\in alpha\to \mathrm{NNReal},D\left(q,p\right)=\mathrm{ite}\left(\forall z\in alpha,(p\left(z\right)=0)\Rightarrow (q\left(z\right)=0),(\sum _{z:alpha}(\frac{(q\left(z\right):\mathbb{R})\cdot \mathrm{Real}.\log \left(\frac{(q\left(z\right):\mathbb{R})}{(p\left(z\right):\mathbb{R})}\right)}{\mathrm{Real}.\log \left(2\right)}):\mathrm{EReal}),\mathrm{Top}.\mathrm{top}\left(\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.D (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Section IV.A, p. 6: “For two (arbitrary) distributions Q and P defined over Z, the Kullback-Leibler (KL) divergence from Q to P is defined as” D(Q∥P) := ∑z∈Z Q(z) log(Q(z)/P(z)), “where the logarithm is taken here, as in the rest of the paper, to base 2.” The zero-mass conventions make a zero q mass contribute zero and a positive q mass above zero p mass contribute infinity. Real.log is the natural logarithm, so division by Real.log 2 converts to bits. The finite branch is coerced from R to EReal; ⊤ is EReal’s positive infinity. The displayed expression uses Lean’s total real division and logarithm, including log 0 = 0, only inside the absolutely continuous branch.

Definition 1.3 (All local response mixtures).

$$\forall s\in \mathbb{N},\forall o\in \mathbb{N},\forall mu\in \mathrm{stdSimplex}\left(\mathrm{NNReal},(\mathrm{Fin}\left(s\right)\to \mathrm{Fin}\left(o\right))\times (\mathrm{Fin}\left(s\right)\to \mathrm{Fin}\left(o\right))\right),\forall x\in \mathrm{Fin}\left(s\right),\forall y\in \mathrm{Fin}\left(s\right),\forall a\in \mathrm{Fin}\left(o\right),\forall b\in \mathrm{Fin}\left(o\right),\mathrm{localBehavior}\left(mu\right)\left(x,y,a,b\right)=\sum _{t:(\mathrm{Fin}\left(s\right)\to \mathrm{Fin}\left(o\right))\times (\mathrm{Fin}\left(s\right)\to \mathrm{Fin}\left(o\right))}(\mathrm{ite}\left((t.1\left(x\right)=a)\wedge (t.2\left(y\right)=b),mu\left(t\right),0\right))$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.localBehavior (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Section II.D, p. 5: “A local theory π may be viewed as a probability distribution for (X₁,X₂,Y₁,Y₂).” For s settings and o outcomes, the literal generalization is: μ is any normalized distribution on pairs of deterministic response functions Fin s → Fin o. The finite sum marginalizes the responses at x and y. It includes every local theory, including nonrational weights; the proof never limits μ to a list of strategies.

Definition 1.4 (Independent setting laws).

$$\forall s\in \mathbb{N},\forall alpha\in \mathrm{stdSimplex}\left(\mathrm{NNReal},\mathrm{Fin}\left(s\right)\right),\forall beta\in \mathrm{stdSimplex}\left(\mathrm{NNReal},\mathrm{Fin}\left(s\right)\right),\forall z\in \mathrm{Fin}\left(s\right)\times \mathrm{Fin}\left(s\right),\mathrm{productLaw}\left(alpha,beta\right)\left(z\right)=alpha\left(z.1\right)\cdot beta\left(z.2\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.productLaw (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Section IV.B, p. 8 requires that “the distribution for each party is uncorrelated with the distributions of the other parties”. Two marginal distributions alpha and beta yield their pointwise product on pairs of settings. The stdSimplex proofs verify its normalization.

Definition 1.5 (Uniform pairs of settings).

$$\forall s\in \mathbb{N},[\mathrm{NeZero}\left(s\right)]\mathrm{uniformLaw}\left(s\right)=\mathrm{productLaw}\left(\mathrm{uniform}\left(s\right),\mathrm{uniform}\left(s\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.uniformLaw (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

This is the source’s σ°: the product of the two uniform setting laws, with s² equally weighted pairs.

Definition 1.6 (Settings and outcomes in one distribution).

$$\forall s\in \mathbb{N},\forall o\in \mathbb{N},\forall sigma\in \mathrm{stdSimplex}\left(\mathrm{NNReal},\mathrm{Fin}\left(s\right)\times \mathrm{Fin}\left(s\right)\right),\forall q\in \mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(o\right)\to \left(\mathrm{Fin}\left(o\right)\to \mathrm{NNReal}\right)\right)\right),\forall z\in (\mathrm{Fin}\left(s\right)\times \mathrm{Fin}\left(s\right))\times (\mathrm{Fin}\left(o\right)\times \mathrm{Fin}\left(o\right)),\mathrm{joint}\left(sigma,q\right)\left(z\right)=sigma\left(z.1\right)\cdot q\left(z.1.1,z.1.2,z.2.1,z.2.2\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.joint (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Section II.B, p. 5: “According to QM, the total outcome (X,Y,A,B) of a single trial is then distributed as Qσ, defined by” Qσ(X = x,Y = y,A = a,B = b) := σab Qab(X = x,Y = y). The index z groups the setting pair z.1 and the outcome pair z.2. Its four entries are selected using Lean’s product projections. q is the conditional outcome law; sigma is a distribution of settings.

Definition 1.7 (Infimum over every local theory).

$$\forall s\in \mathbb{N},\forall o\in \mathbb{N},\forall q\in \mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(o\right)\to \left(\mathrm{Fin}\left(o\right)\to \mathrm{NNReal}\right)\right)\right),\forall sigma\in \mathrm{stdSimplex}\left(\mathrm{NNReal},\mathrm{Fin}\left(s\right)\times \mathrm{Fin}\left(s\right)\right),\mathrm{strengthAt}\left(q,sigma\right)={\mathrm{iInf}}_{mu:\mathrm{stdSimplex}\left(\mathrm{NNReal},(\mathrm{Fin}\left(s\right)\to \mathrm{Fin}\left(o\right))\times (\mathrm{Fin}\left(s\right)\to \mathrm{Fin}\left(o\right))\right)}(D\left(\mathrm{joint}\left(sigma,q\right),\mathrm{joint}\left(sigma,\mathrm{localBehavior}\left(mu\right)\right)\right))$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.strengthAt (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Section IV.B, p. 8 defines D(Qσ∥Pσ) as the infimum of D(Qσ∥Pσ,π) over π∈Π. Here iInf is the infimum in EReal, over the entire stdSimplex of deterministic-response mixtures.

Definition 1.8 (Strength for uniform settings).

$$\forall s\in \mathbb{N},\forall o\in \mathbb{N},[\mathrm{NeZero}\left(s\right)]\forall q\in \mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(o\right)\to \left(\mathrm{Fin}\left(o\right)\to \mathrm{NNReal}\right)\right)\right),S_{uni}\left(q\right)=\mathrm{strengthAt}\left(q,\mathrm{uniformLaw}\left(s\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.S_uni (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Definition 1, Section IV.B, p. 8: “When each measurement setting is sampled with equal probability, the resulting strength S_Q^UNI is defined by” S_Q^UNI := D(Qσ°∥Pσ°) = infπ∈Π D(Qσ°∥Pσ°,π), “where σ° denotes the uniform distribution over the settings.” The source symbol S_Q^UNI is encoded by S_uni q; strengthAt supplies the infimum.

Definition 1.9 (Strength for uncorrelated settings).

$$\forall s\in \mathbb{N},\forall o\in \mathbb{N},\forall q\in \mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(o\right)\to \left(\mathrm{Fin}\left(o\right)\to \mathrm{NNReal}\right)\right)\right),S\left(q\right)={\mathrm{iSup}}_{alpha:\mathrm{stdSimplex}\left(\mathrm{NNReal},\mathrm{Fin}\left(s\right)\right)}({\mathrm{iSup}}_{beta:\mathrm{stdSimplex}\left(\mathrm{NNReal},\mathrm{Fin}\left(s\right)\right)}(\mathrm{strengthAt}\left(q,\mathrm{productLaw}\left(alpha,beta\right)\right)))$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.S (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Definition 2, Section IV.B, p. 8: “When the experimenter QM is allowed to choose any distribution on measurement settings, as long as the distribution for each party is uncorrelated with the distributions of the other parties, the resulting strength S_Q^UC is defined by” S_Q^UC := supσ∈ΣUC D(Qσ∥Pσ) = supσ∈ΣUC infπ∈Π D(Qσ∥Pσ,π), “where σ∈ΣUC denotes the use of uncorrelated settings.” S q is literally the supremum over pairs of marginal distributions, each giving productLaw alpha beta.

Definition 1.10 (Strength for correlated settings).

$$\forall s\in \mathbb{N},\forall o\in \mathbb{N},\forall q\in \mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(s\right)\to \left(\mathrm{Fin}\left(o\right)\to \left(\mathrm{Fin}\left(o\right)\to \mathrm{NNReal}\right)\right)\right),S_{cor}\left(q\right)={\mathrm{iSup}}_{sigma:\mathrm{stdSimplex}\left(\mathrm{NNReal},\mathrm{Fin}\left(s\right)\times \mathrm{Fin}\left(s\right)\right)}(\mathrm{strengthAt}\left(q,sigma\right))$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.S_cor (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Definition 3, Section IV.B, p. 8: “When the experimeniter QM is allowed to choose any distribution on measurement settings (including correlated distributions), the resulting strength S_Q^COR is defined by” S_Q^COR := supσ∈Σ D(Qσ∥Pσ) = supσ∈Σ infπ∈Π D(Qσ∥Pσ,π), “where σ∈Σ denoted the use of correlated settings.” The words “experimeniter” and “denoted” reproduce the source. S_cor q takes the supremum over all normalized setting laws.

Definition 1.11 (The literal Bell singlet).

$$\forall a\in \mathrm{Fin}\left(2\right),\forall b\in \mathrm{Fin}\left(2\right),\mathrm{singletCoefficient}\left(a,b\right)=\mathrm{ite}\left((a=0)\wedge (b=1),(\mathrm{Real}.\mathrm{sqrt}\left(2\right):\mathbb{C}{)}^{-1},\mathrm{ite}\left((a=1)\wedge (b=0),-(\mathrm{Real}.\mathrm{sqrt}\left(2\right):\mathbb{C}{)}^{-1},0\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.singletCoefficient (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

The two-qubit singlet is (|01⟩−|10⟩)/sqrt 2. These are its literal complex amplitudes in the computational basis. The minus sign distinguishes the singlet from Phi-plus. The inverse square root is in C.

Definition 1.12 (Two singlets shared between the parties).

$$\forall z\in (\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathrm{twoSinglets}\left(z\right)=\mathrm{singletCoefficient}\left(z.1.1,z.2.1\right)\cdot \mathrm{singletCoefficient}\left(z.1.2,z.2.2\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.twoSinglets (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

The global index z consists of Alice’s two-qubit basis index z.1 and Bob’s z.2. Multiplying singletCoefficient on each corresponding Alice–Bob pair is the literal tensor product of two singlets, regrouped by party. No entanglement proxy replaces that state.

Definition 1.13 (Four nonzero orthogonal projectors).

$$\forall n\in Type,[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall P\in \mathrm{Fin}\left(4\right)\to \mathrm{Matrix}\left(n,n,\mathbb{C}\right),\mathrm{IsPVM}\left(P\right)=\left((\forall a\in \mathrm{Fin}\left(4\right),(P\left(a\right)\ne 0)\wedge ((\mathrm{star}\left(P\left(a\right)\right)=P\left(a\right))\wedge (P\left(a\right)\cdot P\left(a\right)=P\left(a\right))))\wedge ((\forall a\in \mathrm{Fin}\left(4\right),\forall b\in \mathrm{Fin}\left(4\right),(a\ne b)\Rightarrow (P\left(a\right)\cdot P\left(b\right)=0))\wedge (\sum _{a:\mathrm{Fin}\left(4\right)}(P\left(a\right))=1))\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.IsPVM (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Under the four-nonzero-outcome measurement convention, each setting has four nonzero projectors. Each projector is self-adjoint and idempotent; distinct outcomes are orthogonal; their sum is the identity. star on matrices is conjugate transpose. The anonymous Fintype and DecidableEq brackets are Lean instance arguments, not new mathematical variables.

Definition 1.14 (Two parties, four settings, four outcomes).

$$\begin{array}{r}\mathrm{Experiment}:Type\\ \forall e\in \mathrm{Experiment},\mathrm{Experiment}.\mathrm{alice}\left(e\right):\mathrm{Fin}\left(4\right)\to \left(\mathrm{Fin}\left(4\right)\to \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right)\right)\\ \forall e\in \mathrm{Experiment},\mathrm{Experiment}.\mathrm{bob}\left(e\right):\mathrm{Fin}\left(4\right)\to \left(\mathrm{Fin}\left(4\right)\to \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right)\right)\end{array}$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.Experiment (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

The structure has exactly the fields alice and bob, both with type Fin 4 → Fin 4 → Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) C. The first argument indexes a local setting and the second an outcome. Each party’s operator acts jointly on its two qubits. Together with Valid, this is the source’s 2×4×4 experiment type.

Definition 1.15 (Peres–Mermin observable grid).

$$\begin{array}{r}\mathrm{square}:\mathrm{Fin}\left(3\right)\to \left(\mathrm{Fin}\left(3\right)\to \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right)\right)\\ \mathrm{square}=\left[\begin{array}{ccc}\mathrm{Matrix}.\mathrm{kronecker}\left(\mathrm{qubitZ},1\right)& \mathrm{Matrix}.\mathrm{kronecker}\left(1,\mathrm{qubitZ}\right)& \mathrm{Matrix}.\mathrm{kronecker}\left(\mathrm{qubitZ},\mathrm{qubitZ}\right)\\ \mathrm{Matrix}.\mathrm{kronecker}\left(1,\mathrm{qubitX}\right)& \mathrm{Matrix}.\mathrm{kronecker}\left(\mathrm{qubitX},1\right)& \mathrm{Matrix}.\mathrm{kronecker}\left(\mathrm{qubitX},\mathrm{qubitX}\right)\\ \mathrm{Matrix}.\mathrm{kronecker}\left(\mathrm{qubitZ},\mathrm{qubitX}\right)& \mathrm{Matrix}.\mathrm{kronecker}\left(\mathrm{qubitX},\mathrm{qubitZ}\right)& \mathrm{Matrix}.\mathrm{kronecker}\left(\mathrm{pauliMatrix}\left(\mathrm{Pauli}.Y\right),\mathrm{pauliMatrix}\left(\mathrm{Pauli}.Y\right)\right)\end{array}\right]\end{array}$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.square (✓ std3).

Source. Repository-derived.

Commentary.

The nine entries form the Peres–Mermin square. Matrix.kronecker acts on the two-qubit product indices; 1 is the single-qubit identity matrix.

Definition 1.16 (Validity of all eight settings).

$$\forall e\in \mathrm{Experiment},\mathrm{Valid}\left(e\right)=\left((\forall x\in \mathrm{Fin}\left(4\right),\mathrm{IsPVM}\left(\mathrm{Experiment}.\mathrm{alice}\left(e,x\right)\right))\wedge (\forall y\in \mathrm{Fin}\left(4\right),\mathrm{IsPVM}\left(\mathrm{Experiment}.\mathrm{bob}\left(e,y\right)\right))\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.Valid (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Every Alice setting and every Bob setting satisfies IsPVM. In particular the four outcomes of every setting are nonzero.

Definition 1.17 (Products of single-qubit operators).

$$\forall P\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{ProductOperator}\left(P\right)=\left(\exists A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\exists B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),P=\mathrm{Matrix}.\mathrm{kroneckerMap}\left((\lambda (uv:\mathbb{C}),u\cdot v),A,B\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.ProductOperator (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

A product operator is literally a Kronecker product A ⊗ₖ B of arbitrary two-by-two complex matrices. No rank or separability surrogate replaces that existential definition.

Definition 1.18 (A joint measurement on a pair).

$$\forall e\in \mathrm{Experiment},\mathrm{JointMeasurement}\left(e\right)=\left((\exists x\in \mathrm{Fin}\left(4\right),\exists a\in \mathrm{Fin}\left(4\right),\neg \mathrm{ProductOperator}\left(\mathrm{Experiment}.\mathrm{alice}\left(e,x,a\right)\right))\vee (\exists y\in \mathrm{Fin}\left(4\right),\exists b\in \mathrm{Fin}\left(4\right),\neg \mathrm{ProductOperator}\left(\mathrm{Experiment}.\mathrm{bob}\left(e,y,b\right)\right))\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.JointMeasurement (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Conjecture 5, Section VI.D, p. 11 requires “involving joint measurements on the pairs.” This means that at least one local projector, for Alice or Bob, is not a product of single-qubit operators. The existential quantifiers range over actual settings and outcomes.

Definition 1.19 (Born amplitudes of the two-singlet experiment).

$$\forall e\in \mathrm{Experiment},\forall x\in \mathrm{Fin}\left(4\right),\forall y\in \mathrm{Fin}\left(4\right),\forall a\in \mathrm{Fin}\left(4\right),\forall b\in \mathrm{Fin}\left(4\right),\mathrm{born}\left(e,x,y,a,b\right)=\mathrm{dotProduct}\left(\mathrm{star}\left(\mathrm{twoSinglets}\right),\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{Matrix}.\mathrm{kroneckerMap}\left((\lambda (uv:\mathbb{C}),u\cdot v),\mathrm{Experiment}.\mathrm{alice}\left(e,x,a\right),\mathrm{Experiment}.\mathrm{bob}\left(e,y,b\right)\right),\mathrm{twoSinglets}\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.born (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

The expression is the literal Born expectation: dotProduct of star twoSinglets with the action of the Kronecker product of the two local outcome projectors. All four indices range over Fin 4.

Definition 1.20 (Conditional quantum probabilities).

$$\forall e\in \mathrm{Experiment},\forall x\in \mathrm{Fin}\left(4\right),\forall y\in \mathrm{Fin}\left(4\right),\forall a\in \mathrm{Fin}\left(4\right),\forall b\in \mathrm{Fin}\left(4\right),\mathrm{quantum}\left(e\right)\left(x,y,a,b\right)=\mathrm{Real}.\mathrm{toNNReal}\left(\mathrm{Complex}.\mathrm{re}\left(\mathrm{born}\left(e,x,y,a,b\right)\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.quantum (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

The quantum conditional law is Real.toNNReal of the real part of the Born expectation. Validity proves that this real part is nonnegative and that the probabilities sum to one; the truncation thus leaves every valid Born probability unchanged.

Definition 1.21 (Alice’s CHSH projectors).

$$\forall x\in \mathrm{Fin}\left(2\right),\forall a\in \mathrm{Fin}\left(2\right),\mathrm{chshAlice}\left(x,a\right)=\mathrm{HSMul}.\mathrm{hSMul}\left((\frac{1}{2}:\mathbb{C}),1+\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{ite}\left(a=0,1,-1\right),\mathrm{ite}\left(x=0,\mathrm{qubitZ},\mathrm{qubitX}\right)\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.chshAlice (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Appendix III.C, pp. 18–20 gives the CHSH quantum table. These two-outcome projectors use frozen qubitZ and qubitX. Settings and outcomes have indices 0 and 1. The sign is +1 for outcome 0 and −1 for outcome 1.

Definition 1.22 (Bob’s singlet-conjugated CHSH projectors).

$$\forall y\in \mathrm{Fin}\left(2\right),\forall b\in \mathrm{Fin}\left(2\right),\mathrm{chshBob}\left(y,b\right)=\mathrm{HSMul}.\mathrm{hSMul}\left((\frac{1}{2}:\mathbb{C}),1+\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{ite}\left(b=0,1,-1\right),\mathrm{HSMul}.\mathrm{hSMul}\left(-(\mathrm{Real}.\mathrm{sqrt}\left(2\right):\mathbb{C}{)}^{-1},\mathrm{ite}\left(y=0,\mathrm{qubitZ}+\mathrm{qubitX},\mathrm{qubitZ}-\mathrm{qubitX}\right)\right)\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.chshBob (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

The source realizes its CHSH table with Phi-plus. Bob’s observables are conjugated by the local singlet unitary. On a literal singlet they are −(Z+X)/sqrt 2 and −(Z−X)/sqrt 2; these projectors reproduce the source table, with probabilities (2+sqrt 2)/8 for a winning output and (2−sqrt 2)/8 otherwise.

Definition 1.23 (The CHSH Born expectation on a singlet).

$$\forall x\in \mathrm{Fin}\left(2\right),\forall y\in \mathrm{Fin}\left(2\right),\forall a\in \mathrm{Fin}\left(2\right),\forall b\in \mathrm{Fin}\left(2\right),\mathrm{chshBorn}\left(x,y,a,b\right)=\mathrm{dotProduct}\left(\mathrm{star}\left((\lambda (z:\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathrm{singletCoefficient}\left(z.1,z.2\right))\right),\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{Matrix}.\mathrm{kroneckerMap}\left((\lambda (uv:\mathbb{C}),u\cdot v),\mathrm{chshAlice}\left(x,a\right),\mathrm{chshBob}\left(y,b\right)\right),(\lambda (z:\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathrm{singletCoefficient}\left(z.1,z.2\right))\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.chshBorn (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

The vector in both dotProduct and mulVec has entries singletCoefficient z.1 z.2. This expectation uses a literal singlet and the displayed CHSH PVMs, not the source’s Phi-plus state.

Definition 1.24 (The physical CHSH conditional law).

$$\forall x\in \mathrm{Fin}\left(2\right),\forall y\in \mathrm{Fin}\left(2\right),\forall a\in \mathrm{Fin}\left(2\right),\forall b\in \mathrm{Fin}\left(2\right),\mathrm{chsh}\left(x,y,a,b\right)=\mathrm{Real}.\mathrm{toNNReal}\left(\mathrm{Complex}.\mathrm{re}\left(\mathrm{chshBorn}\left(x,y,a,b\right)\right)\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.chsh (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

The probabilities are Real.toNNReal of the real parts of the literal singlet Born expectations. The private source_chsh_born calculation connects this law to Appendix III.C’s table and is used in the arbitrary-setting-law upper bound.

Definition 1.25 (Conjecture 5).

$$\exists e\in \mathrm{Experiment},(\mathrm{Valid}\left(e\right))\wedge ((\mathrm{JointMeasurement}\left(e\right))\wedge (S_{uni}\left(\mathrm{quantum}\left(e\right)\right)>2\cdot S_{cor}\left(\mathrm{chsh}\right)))$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.claim (✓ std3).

Citation. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

Conjecture 5, Section VI.D, p. 11: “There is an experiment on pairs of Bell singlets, of the 2×4×4 type, more than twice as strong as CHSH, and involving joint measurements on the pairs.” The encoding is: there exists e : Experiment with Valid e and JointMeasurement e, and S_uni (quantum e) > 2 * S_cor chsh. Since the uniform strength is no larger than the product-setting strength, which is no larger than the correlated-setting strength, this inequality implies the required comparison in each of the source’s three senses.

Definition 1.26 (Rational amplitudes of two singlets).

$$\forall z\in (\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathrm{rationalSinglets}\left(z\right)=\mathrm{ite}\left((z.1.1\ne z.2.1)\wedge (z.1.2\ne z.2.2),\mathrm{ite}\left(z.1.1=z.1.2,(\frac{1}{2}:\mathbb{C}),-\frac{1}{2}\right),0\right)$$

Formalization. D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.rationalSinglets (✓ std3).

Source. Repository-derived.

Acknowledgement. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

For each party-grouped basis index z, the amplitude is zero unless both corresponding bit pairs differ. When both differ, equal bits on Alice’s side give one half and unequal bits give minus one half. These are the rational amplitudes of the product of two singlets.

Theorem 1.27 (The two-singlet experiment proves the conjecture).

$$\exists e\in \mathrm{Experiment},(\mathrm{Valid}\left(e\right))\wedge ((\mathrm{JointMeasurement}\left(e\right))\wedge (S_{uni}\left(\mathrm{quantum}\left(e\right)\right)>2\cdot S_{cor}\left(\mathrm{chsh}\right)))$$

Proof. Machine-checked in Lean as D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.result (✓ std3). ∎

Resolves. Problems/van-dam-gill-grunwald-2005-two-singlet-strength (proved) by D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.result.

Source. Repository-derived.

Acknowledgement. W. van Dam; R. D. Gill; P. D. Grünwald (2005). The Statistical Strength of Nonlocality Proofs. DOI: 10.1109/TIT.2005.851738. URL: https://arxiv.org/abs/quant-ph/0307125v2.

Commentary.

The commuting magic-square rows and columns give four nonzero-outcome PVMs on each side. Bob’s transpose and local singlet conjugation give the Born trace identity, and losing parity outcomes have zero probability. Every pair of deterministic local response functions wins at most eight of the nine magic-square contexts. Averaging preserves that bound for every normalized local mixture. Coarse-graining the uniform joint law into outside, winning and losing bins and applying the frozen log-sum inequality proves S_uni ≥ (9/16) log(9/8)/log 2. A single local CHSH reference mixture gives S_cor CHSH ≤ c for every setting law. The fulfilled rational logarithm enclosures prove 2c < 93/1000 < 95/1000 < (9/16) log(9/8)/log 2. A nonzero product-operator minor proves that an Alice projector is joint. No exact optimal strength or global optimality claim is made.

References

• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.D
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.Experiment
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.IsPVM
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.JointMeasurement
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.ProductOperator
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.S
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.S_cor
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.S_uni
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.Valid
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.born
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.chsh
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.chshAlice
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.chshBob
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.chshBorn
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.claim
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.joint
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.localBehavior
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.productLaw
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.quantum
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.rationalSinglets
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.result
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.singletCoefficient
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.square
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.strengthAt
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.twoSinglets
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.uniform
• Truth anchor: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare.uniformLaw
• Dependency: D5/S3/DivergenceSupport/LogSumInequality
• Dependency: D5/S3/Entropy/Forgetting/CapacityMonotone
• Dependency: D5/S3/Quantum/Information/StabilizerPairLocalUnitaryInequivalence