CHSH_inequality_of_comm
theorem CHSH_inequality_of_comm :
∀ {R : Type u} [inst : OrderedCommRing R] [inst_1 : StarRing R] [inst_2 : StarOrderedRing R] [inst_3 : Algebra ℝ R]
[inst_4 : OrderedSMul ℝ R] (A₀ A₁ B₀ B₁ : R),
IsCHSHTuple A₀ A₁ B₀ B₁ → A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
The theorem states that for any commutative ordered star-algebra over the real numbers ℝ, given a Clauser-Horne-Shimony-Holt (CHSH) tuple (A₀, A₁, B₀, B₁), the sum of the products A₀ * B₀, A₀ * B₁, A₁ * B₀ minus the product A₁ * B₁ is less than or equal to 2. Notably, this theorem could also be applied in the context of the ring of integers with one-half, ℤ[½].
More concisely: In any commutative ordered star-algebra over the real numbers, the sum of the products of any CHSH tuple's elements is bounded by 2.
|
tsirelson_inequality
theorem tsirelson_inequality :
∀ {R : Type u} [inst : OrderedRing R] [inst_1 : StarRing R] [inst_2 : StarOrderedRing R] [inst_3 : Algebra ℝ R]
[inst_4 : OrderedSMul ℝ R] [inst_5 : StarModule ℝ R] (A₀ A₁ B₀ B₁ : R),
IsCHSHTuple A₀ A₁ B₀ B₁ → A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1
This theorem, known as Tsirelson's inequality, states that in a noncommutative ordered `*`-algebra over the real numbers (ℝ), the maximum value of the CHSH tuple (A₀, A₁, B₀, B₁) is bounded by `2^(3/2)`. In other words, the value of `A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁` is always less than or equal to `2^(3/2)`, assuming that (A₀, A₁, B₀, B₁) is a CHSH tuple. The proof involves an explicit sum-of-squares decomposition of the difference between the two sides of the inequality. This principle could also theoretically be demonstrated using the ring of integers extended by `2^(1/2)` and `2^(-1/2)` if desired.
More concisely: In a noncommutative ordered `*`-algebra over the real numbers, the maximum value of the CHSH expression `A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁` is bounded by `2^(3/2)`.
|