English
An explicit CHSH expression built from A0, A1, B0, B1 satisfies the square identity P^2 = 4P, where P is the CHSH combination.
Русский
Явление CHSH с участием A0, A1, B0, B1 удовлетворяет квадратному тождеству P^2 = 4P, где P — CHSH-выражение.
LaTeX
$$$\\Big(2 - A_0 B_0 - A_0 B_1 - A_1 B_0 + A_1 B_1\\Big)^2 = 4 \\Big(2 - A_0 B_0 - A_0 B_1 - A_1 B_0 + A_1 B_1\\Big).$$$
Lean4
theorem CHSH_id [CommRing R] {A₀ A₁ B₀ B₁ : R} (A₀_inv : A₀ ^ 2 = 1) (A₁_inv : A₁ ^ 2 = 1) (B₀_inv : B₀ ^ 2 = 1)
(B₁_inv : B₁ ^ 2 = 1) :
(2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) :=
by grind
