English
For a CHSH tuple in a commutative ordered *-algebra over R with appropriate structure, the CHSH expression is bounded by 2: A0B0 + A0B1 + A1B0 − A1B1 ≤ 2.
Русский
Для CHSH-узла в коммутативном упорядоченном *-алгебре над R существует верхняя граница: A0B0 + A0B1 + A1B0 − A1B1 ≤ 2.
LaTeX
$$$A_0 B_0 + A_0 B_1 + A_1 B_0 - A_1 B_1 \le 2$$$
Lean4
/-- Given a CHSH tuple (A₀, A₁, B₀, B₁) in a *commutative* ordered `*`-algebra over ℝ,
`A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2`.
(We could work over ℤ[⅟2] if we wanted to!)
-/
theorem CHSH_inequality_of_comm [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [Algebra ℝ R]
[IsOrderedModule ℝ R] (A₀ A₁ B₀ B₁ : R) (T : IsCHSHTuple A₀ A₁ B₀ B₁) : A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2 :=
by
let P := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
have i₁ : 0 ≤ P := by
have idem : P * P = 4 * P := CHSH_id T.A₀_inv T.A₁_inv T.B₀_inv T.B₁_inv
have idem' : P = (1 / 4 : ℝ) • (P * P) :=
by
have h : 4 * P = (4 : ℝ) • P := by simp [map_ofNat, Algebra.smul_def]
rw [idem, h, ← mul_smul]
simp
have sa : star P = P := by
dsimp [P]
simp only [star_add, star_sub, star_mul, star_ofNat, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa, mul_comm B₀, mul_comm B₁]
simpa only [← idem', sa] using smul_nonneg (by simp : (0 : ℝ) ≤ 1 / 4) (star_mul_self_nonneg P)
apply le_of_sub_nonneg
simpa only [sub_add_eq_sub_sub, ← sub_add] using i₁
