Quantum foundations

Quantum foundations studies what quantum mechanics rules out and allows at the level of measurement outcomes, including contextuality, Bell nonlocality and bounds on quantum correlations.

TheoremKochen–Specker theorem in \(\mathbb{R}^3\)#✓fully proved

There exist a natural number \(N\) and unit vectors \(v_1, \dots, v_N \in \mathbb{R}^3\) such that no function \(c : \{1, \dots, N\} \to \{0, 1\}\) satisfies both of the following: \(c(i) + c(j) \le 1\) whenever \(v_i\) and \(v_j\) are orthogonal, and \(c(i) + c(j) + c(k) = 1\) whenever \((v_i, v_j, v_k)\) is an orthonormal triple.

theorem kochen_specker_finite_real_three :
    ∃ (N : ℕ) (v : Fin N → EuclideanSpace ℝ (Fin 3)),
      (∀ i, ‖v i‖ = 1) ∧
      ¬ ∃ (c : Fin N → Fin 2),
        (∀ i j : Fin N, inner (𝕜 := ℝ) (v i) (v j) = 0 →
          (c i).val + (c j).val ≤ 1) ∧
          ∀ (b : Fin 3 → Fin N),
            Orthonormal ℝ (fun r => v (b r)) →
              (∑ r : Fin 3, (c (b r)).val) = 1
Sources
  • S. Kochen, E. P. Specker, The Problem of Hidden Variables in Quantum Mechanics, J. Math. Mech. 17 (1967), 59-87, DOI 10.1512/iumj.1968.17.17004.

TheoremTsirelson's bound is attained#✓fully proved

There exist \(4 \times 4\) complex matrices \(A_0, A_1, B_0, B_1\) such that each of them is Hermitian and squares to the identity matrix, each \(A_i\) commutes with each \(B_j\), and the CHSH operator \(A_0 B_0 + A_0 B_1 + A_1 B_0 - A_1 B_1\) has \(2\sqrt{2}\) as an eigenvalue.

This shows that the upper bound \(2\sqrt{2}\) in Tsirelson's inequality for CHSH tuples is sharp.

public theorem tsirelson_bound_tight :
    ∃ (A₀ A₁ B₀ B₁ : Matrix (Fin 4) (Fin 4) ℂ),
      IsCHSHTuple A₀ A₁ B₀ B₁ ∧
        Module.End.HasEigenvalue
          (Matrix.toLin' (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁))
          ((↑(2 * Real.sqrt 2) : ℂ))
Sources
  • B. S. Cirel'son/Tsirelson, "Quantum generalizations of Bell's inequality", Lett. Math. Phys. 4 (1980), 93-100, DOI 10.1007/BF00417500.
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.