Temporal Hardy attainment for every positive spin

Abstract

For every positive integer n, spin-n/2 measurements attain temporal Hardy success probability one quarter.

Work on ℂ^(n+1) in the standard basis e_k = |n/2 − k⟩, with ℏ = 1. The matrices Jx(n), Jy(n) and Jz(n) are the spin-n/2 components in this basis. Fin(n+1) indexes the coordinates from zero through n. A matrix asterisk denotes the conjugate transpose, and a real scalar in a complex matrix or vector expression is included into ℂ.

Definition 1.1 (A scaled outer product).

$$\forall (n:\mathbb{N}),(\forall (w:(\mathrm{Fin}\left((n+1)\right)\to \mathbb{C})),(\forall (d:\mathbb{R}),(\mathrm{ray}\left(n,w,d\right)=(d:\mathbb{C}{)}^{-1}\cdot \mathrm{vecMulVec}\left(w,\mathrm{star}\left(w\right)\right))))$$

Formalization. D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.ray (✓ std3).

Source. Repository-derived.

Commentary.

The outer product of w with its conjugate is scaled by the inverse of the real normalization parameter, included into ℂ.

Definition 1.2 (A spin component in a real direction).

$$\forall (n:\mathbb{N}),(\forall (u:(\mathrm{Fin}\left(3\right)\to \mathbb{R})),(\mathrm{spinComponent}\left(n,u\right)=\mathrm{ofReal}\left(u\left(0\right)\right)\cdot \mathrm{Jx}\left(n\right)+\mathrm{ofReal}\left(u\left(1\right)\right)\cdot \mathrm{Jy}\left(n\right)+\mathrm{ofReal}\left(u\left(2\right)\right)\cdot \mathrm{Jz}\left(n\right)))$$

Formalization. D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.spinComponent (✓ std3).

Citation. Sujit K. Choudhary; Sandeep K. Goyal; Thomas Konrad; Sibasish Ghosh (2013). Persistence of Hardy’s nonlocality in time. URL: https://arxiv.org/abs/1302.5296v1.

Commentary.

The spin component u·S is u₀Jx(n) + u₁Jy(n) + u₂Jz(n). This definition allows every real direction u; the unit-length conditions for the four measurement directions appear in claim.

Theorem 1.3 (Binomial spin ladder coefficients).

$$\forall (n:\mathbb{N}),(\forall (k:\mathbb{N}),((k<n)\Rightarrow ((\mathrm{sqrt}\left(\left((\mathrm{cast}\left(k\right):\mathbb{R})+1\right)\cdot \left((\mathrm{cast}\left(n\right):\mathbb{R})-(\mathrm{cast}\left(k\right):\mathbb{R})\right)\right)\cdot \mathrm{sqrt}\left((\mathrm{cast}\left(\mathrm{choose}\left(n,k+1\right)\right):\mathbb{R})\right)=\left((\mathrm{cast}\left(n\right):\mathbb{R})-(\mathrm{cast}\left(k\right):\mathbb{R})\right)\cdot \mathrm{sqrt}\left((\mathrm{cast}\left(\mathrm{choose}\left(n,k\right)\right):\mathbb{R})\right))\wedge (\mathrm{sqrt}\left(\left((\mathrm{cast}\left(k\right):\mathbb{R})+1\right)\cdot \left((\mathrm{cast}\left(n\right):\mathbb{R})-(\mathrm{cast}\left(k\right):\mathbb{R})\right)\right)\cdot \mathrm{sqrt}\left((\mathrm{cast}\left(\mathrm{choose}\left(n,k\right)\right):\mathbb{R})\right)=\left((\mathrm{cast}\left(k\right):\mathbb{R})+1\right)\cdot \mathrm{sqrt}\left((\mathrm{cast}\left(\mathrm{choose}\left(n,k+1\right)\right):\mathbb{R})\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.ladder_pair (✓ std3). ∎

Source. Repository-derived.

Commentary.

For k < n, the spin ladder coefficient relates the square roots of two adjacent binomial coefficients in both directions.

Theorem 1.4 (Entries of the raising matrix).

$$\forall (n:\mathbb{N}),(\forall (i:\mathrm{Fin}\left((n+1)\right)),(\forall (j:\mathrm{Fin}\left((n+1)\right)),(\mathrm{Jplus}\left(n,i,j\right)=\{\begin{array}{ll}\mathrm{ofReal}\left(\mathrm{sqrt}\left((\mathrm{cast}\left(\mathrm{val}\left(j\right)\right):\mathbb{R})\cdot \left((\mathrm{cast}\left(n\right):\mathbb{R})+1-(\mathrm{cast}\left(\mathrm{val}\left(j\right)\right):\mathbb{R})\right)\right)\right)& \mathrm{val}\left(i\right)+1=\mathrm{val}\left(j\right)\\ 0& \text{otherwise}\end{array})))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.raising_entry (✓ std3). ∎

Source. Repository-derived.

Commentary.

The raising matrix has the square-root spin coefficient on its superdiagonal and zero elsewhere.

Definition 1.5 (Real binomial coefficients).

$$\forall (n:\mathbb{N}),(\forall (r:\mathbb{R}),(\forall (k:\mathrm{Fin}\left((n+1)\right)),(\mathrm{coeff}\left(n,r,k\right)=\mathrm{sqrt}\left((\mathrm{cast}\left(\mathrm{choose}\left(n,\mathrm{val}\left(k\right)\right)\right):\mathbb{R})\right)\cdot r^{\mathrm{val}\left(k\right)})))$$

Formalization. D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.coeff (✓ std3).

Citation. Sujit K. Choudhary; Sandeep K. Goyal; Thomas Konrad; Sibasish Ghosh (2013). Persistence of Hardy’s nonlocality in time. URL: https://arxiv.org/abs/1302.5296v1.

Commentary.

For every n, every real r and every index k, coeff(n,r,k)=√C(n,k) r^k. No positivity or nonzero assumption on r is imposed.

Definition 1.6 (The complex binomial vector).

$$\forall (n:\mathbb{N}),(\forall (r:\mathbb{R}),(\forall (k:\mathrm{Fin}\left((n+1)\right)),(\mathrm{binomVector}\left(n,r,k\right)=\mathrm{ofReal}\left(\mathrm{coeff}\left(n,r,k\right)\right))))$$

Formalization. D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.binomVector (✓ std3).

Citation. Sujit K. Choudhary; Sandeep K. Goyal; Thomas Konrad; Sibasish Ghosh (2013). Persistence of Hardy’s nonlocality in time. URL: https://arxiv.org/abs/1302.5296v1.

Commentary.

The real coefficient vector is included coordinatewise into the complete complex spin space.

Theorem 1.7 (Raising a binomial vector).

$$\forall (n:\mathbb{N}),(\forall (r:\mathbb{R}),(\forall (i:\mathrm{Fin}\left((n+1)\right)),(\mathrm{mulVec}\left(\mathrm{Jplus}\left(n\right),\mathrm{binomVector}\left(n,r\right)\right)\left(i\right)=\left(\mathrm{ofReal}\left((\mathrm{cast}\left(n\right):\mathbb{R})\right)-\mathrm{ofReal}\left((\mathrm{cast}\left(\mathrm{val}\left(i\right)\right):\mathbb{R})\right)\right)\cdot \mathrm{ofReal}\left(r\right)\cdot \mathrm{binomVector}\left(n,r\right)\left(i\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.raising_action (✓ std3). ∎

Source. Repository-derived.

Commentary.

This coordinate identity holds for every n, every real r and every index i, including the last index where raising vanishes.

Theorem 1.8 (Lowering a binomial vector).

$$\forall (n:\mathbb{N}),(\forall (r:\mathbb{R}),(\forall (i:\mathrm{Fin}\left((n+1)\right)),(\mathrm{mulVec}\left((\mathrm{Jplus}\left(n\right){)}^{\ast },\mathrm{binomVector}\left(n,r\right)\right)\left(i\right)\cdot \mathrm{ofReal}\left(r\right)=\mathrm{ofReal}\left((\mathrm{cast}\left(\mathrm{val}\left(i\right)\right):\mathbb{R})\right)\cdot \mathrm{binomVector}\left(n,r\right)\left(i\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.lowering_action (✓ std3). ∎

Source. Repository-derived.

Commentary.

The identity is multiplied by r, so it also holds at r=0. It includes the first index where lowering vanishes.

Definition 1.9 (The projector onto an outcome eigenspace).

$$\forall (n:\mathbb{N}),(\forall (M:\mathrm{Matrix}\left(\mathrm{Fin}\left((n+1)\right),\mathrm{Fin}\left((n+1)\right),\mathbb{C}\right)),(\forall (\pi :\mathrm{Matrix}\left(\mathrm{Fin}\left((n+1)\right),\mathrm{Fin}\left((n+1)\right),\mathbb{C}\right)),(\forall (a:\mathbb{R}),((\mathrm{IsSpectralProjector}\left(M,\pi ,a\right))\iff (({\pi }^2=\pi )\wedge (({\pi }^{\ast }=\pi )\wedge (\forall (v:(\mathrm{Fin}\left((n+1)\right)\to \mathbb{C})),((\pi \cdot v=v)\iff (M\cdot v=\mathrm{ofReal}\left(a\right)\cdot v)))))))))$$

Formalization. D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.IsSpectralProjector (✓ std3).

Citation. Sujit K. Choudhary; Sandeep K. Goyal; Thomas Konrad; Sibasish Ghosh (2013). Persistence of Hardy’s nonlocality in time. URL: https://arxiv.org/abs/1302.5296v1.

Commentary.

For complex matrices M and Π and a real outcome a, IsSpectralProjector requires Π to be idempotent and self-adjoint, with fixed vectors exactly the a-eigenvectors of M. Thus its range is the whole a-eigenspace, including any degeneracy, as required for a Lüders measurement in Section III.

Definition 1.10 (The sequential expectation).

$$\forall (n:\mathbb{N}),(\forall (\psi :(\mathrm{Fin}\left((n+1)\right)\to \mathbb{C})),(\forall ({\pi }_X:\mathrm{Matrix}\left(\mathrm{Fin}\left((n+1)\right),\mathrm{Fin}\left((n+1)\right),\mathbb{C}\right)),(\forall ({\pi }_Y:\mathrm{Matrix}\left(\mathrm{Fin}\left((n+1)\right),\mathrm{Fin}\left((n+1)\right),\mathbb{C}\right)),(\mathrm{seqProb}\left(\psi ,{\pi }_X,{\pi }_Y\right)=⟨\psi \mid ({\pi }_X\cdot {\pi }_Y\cdot {\pi }_X)\mid \psi ⟩))))$$

Formalization. D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.seqProb (✓ std3).

Citation. Sujit K. Choudhary; Sandeep K. Goyal; Thomas Konrad; Sibasish Ghosh (2013). Persistence of Hardy’s nonlocality in time. URL: https://arxiv.org/abs/1302.5296v1.

Commentary.

The expression is defined for every complex vector ψ and every pair of complex matrices Π_X and Π_Y. For a unit state and orthogonal outcome projectors it is the sequential probability in Section III: first measure X and then Y. The complementary outcome uses I − Π.

Definition 1.11 (Attainability with spin measurements).

$$(\mathrm{claim})\iff (\forall (n:\mathbb{N}),((1\le n)\Rightarrow (\exists (u_{A1}:(\mathrm{Fin}\left(3\right)\to \mathbb{R})),(\exists (u_{A2}:(\mathrm{Fin}\left(3\right)\to \mathbb{R})),(\exists (u_{B1}:(\mathrm{Fin}\left(3\right)\to \mathbb{R})),(\exists (u_{B2}:(\mathrm{Fin}\left(3\right)\to \mathbb{R})),(\exists (a_1:\mathbb{R}),(\exists (a_2:\mathbb{R}),(\exists (b_1:\mathbb{R}),(\exists (b_2:\mathbb{R}),(\exists ({\pi }_{A1}:\mathrm{Matrix}\left(\mathrm{Fin}\left((n+1)\right),\mathrm{Fin}\left((n+1)\right),\mathbb{C}\right)),(\exists ({\pi }_{A2}:\mathrm{Matrix}\left(\mathrm{Fin}\left((n+1)\right),\mathrm{Fin}\left((n+1)\right),\mathbb{C}\right)),(\exists ({\pi }_{B1}:\mathrm{Matrix}\left(\mathrm{Fin}\left((n+1)\right),\mathrm{Fin}\left((n+1)\right),\mathbb{C}\right)),(\exists ({\pi }_{B2}:\mathrm{Matrix}\left(\mathrm{Fin}\left((n+1)\right),\mathrm{Fin}\left((n+1)\right),\mathbb{C}\right)),(\exists (\psi :(\mathrm{Fin}\left((n+1)\right)\to \mathbb{C})),((\sum _{(i:\mathrm{Fin}\left(3\right))}(\left(u_{A1}\right)\left(i\right){)}^2=1)\wedge ((\sum _{(i:\mathrm{Fin}\left(3\right))}(\left(u_{A2}\right)\left(i\right){)}^2=1)\wedge ((\sum _{(i:\mathrm{Fin}\left(3\right))}(\left(u_{B1}\right)\left(i\right){)}^2=1)\wedge ((\sum _{(i:\mathrm{Fin}\left(3\right))}(\left(u_{B2}\right)\left(i\right){)}^2=1)\wedge ((\mathrm{IsSpectralProjector}\left(\mathrm{spinComponent}\left(n,u_{A1}\right),{\pi }_{A1},a_1\right))\wedge ((\mathrm{IsSpectralProjector}\left(\mathrm{spinComponent}\left(n,u_{A2}\right),{\pi }_{A2},a_2\right))\wedge ((\mathrm{IsSpectralProjector}\left(\mathrm{spinComponent}\left(n,u_{B1}\right),{\pi }_{B1},b_1\right))\wedge ((\mathrm{IsSpectralProjector}\left(\mathrm{spinComponent}\left(n,u_{B2}\right),{\pi }_{B2},b_2\right))\wedge ((⟨\psi ,\psi ⟩=1)\wedge ((\mathrm{seqProb}\left(\psi ,{\pi }_{A1},{\pi }_{B1}\right)=0)\wedge ((\mathrm{seqProb}\left(\psi ,(1-{\pi }_{A1}),{\pi }_{B2}\right)=0)\wedge ((\mathrm{seqProb}\left(\psi ,{\pi }_{A2},(1-{\pi }_{B1})\right)=0)\wedge (\mathrm{seqProb}\left(\psi ,{\pi }_{A2},{\pi }_{B2}\right)=\frac{1}{4}))))))))))))))))))))))))))))$$

Formalization. D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.claim (✓ std3).

Citation. Sujit K. Choudhary; Sandeep K. Goyal; Thomas Konrad; Sibasish Ghosh (2013). Persistence of Hardy’s nonlocality in time. URL: https://arxiv.org/abs/1302.5296v1.

Commentary.

For every n ≥ 1, there are four real unit directions, four real outcomes, their full spectral projectors, and a unit complex state ψ satisfying the three zero conditions and attaining success probability 1/4. These are the temporal Hardy conditions of Sections II and III, with the attainable value conjectured for every spin in the conclusion and Appendix B. The assertion is attainability; the dimension-independent upper bound is established in Section III of the source.

Theorem 1.12 (A construction attaining one quarter for every positive spin).

$$\mathrm{claim}$$

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

Resolves. Problems/choudhary-goyal-konrad-ghosh-2013-temporal-hardy-spin-attainment (proved) by D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.result.

Source. Repository-derived.

Acknowledgement. Sujit K. Choudhary; Sandeep K. Goyal; Thomas Konrad; Sibasish Ghosh (2013). Persistence of Hardy’s nonlocality in time. URL: https://arxiv.org/abs/1302.5296v1.

Commentary.

Fix n ≥ 1 and put r = √(2^{1/n} − 1), so r > 0 and (1 + r²)^n = 2. Let b_k = √C(n,k) r^k for 0 ≤ k ≤ n, where C(n,k) is the binomial coefficient, and set ψ = b − e₀. The binomial theorem gives ⟨b,b⟩ = 2, while b₀ = 1; hence ⟨ψ,ψ⟩ = 1.

Set a = (1 − r²)/(1 + r²), c = 2r/(1 + r²), and S = a Jz(n) + c Jx(n). Then a² + c² = 1. The spin ladder identities give S b = (n/2)b. The superdiagonal entries of S are strictly positive. Its tridiagonal recurrence forces any eigenvector whose first coordinate vanishes to be zero. Consequently its n/2-eigenspace is exactly span{b}. The diagonal entries of Jz(n) are n/2 − k, so its n/2-eigenspace is exactly span{e₀}. Both eigenspaces are one-dimensional.

Choose A₁ = B₂ = Jz(n), A₂ = B₁ = S, and all four outcomes n/2. Their spectral projectors are P = |e₀⟩⟨e₀| and Q = |b⟩⟨b|/2, respectively. Since Pψ = 0, Qψ = b/2, Pb = e₀ and Qe₀ = b/2, the probabilities ⟨ψ|PQP|ψ⟩, ⟨ψ|(I − P)P(I − P)|ψ⟩ and ⟨ψ|Q(I − Q)Q|ψ⟩ all vanish, whereas ⟨ψ|QPQ|ψ⟩ = 1/4. This realizes the spin-measurement attainability conjecture stated in the conclusion and Appendix B.

References

• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.IsSpectralProjector
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.binomVector
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.claim
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.coeff
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.ladder_pair
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.lowering_action
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.raising_action
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.raising_entry
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.ray
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.result
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.seqProb
• Truth anchor: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment.spinComponent
• Dependency: D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics
• Dependency: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound