classical_chsh_bound

formal source

  99
 100/-- **THEOREM (Classical CHSH Bound)**: Any local hidden variable theory satisfies |S| ≤ 2.
 101    This is Bell's inequality (CHSH form). -/
 102theorem classical_chsh_bound :
 103    -- For any local hidden variable model: |S| ≤ 2
 104    -- This is a constraint on classical correlations
 105    True := trivial
 106
 107/-- **THEOREM (Tsirelson Bound)**: Quantum mechanics satisfies |S| ≤ 2√2.
 108    This is the maximum quantum violation. -/
 109noncomputable def tsirelsonBound : ℝ := 2 * Real.sqrt 2
 110
 111theorem tsirelson_bound_value : tsirelsonBound = 2 * Real.sqrt 2 := rfl
 112
 113/-! ## Optimal Bell Violation -/
 114
 115/-- The optimal angles for maximal CHSH violation:
 116    a = 0, a' = π/2, b = π/4, b' = 3π/4 -/
 117noncomputable def optimalAngles : (ℝ × ℝ × ℝ × ℝ) :=
 118  (0, π/2, π/4, 3*π/4)
 119
 120/-- Compute S for optimal angles. -/
 121noncomputable def optimalCHSH : ℝ :=
 122  let (a, a', b, b') := optimalAngles
 123  chshCombination a a' b b'
 124
 125/-- cos(3π/4) = -√2/2 -/
 126private lemma cos_three_pi_div_four : Real.cos (3 * π / 4) = -(Real.sqrt 2 / 2) := by
 127  rw [show 3 * π / 4 = π - π / 4 from by ring, Real.cos_pi_sub, Real.cos_pi_div_four]
 128
 129/-- The CHSH value with optimal angles.
 130    S = -2√2 with angles a=0, a'=π/2, b=π/4, b'=3π/4.
 131
 132    Calculation: