def
definition
chshCombination
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Quantum.BellInequality on GitHub at line 96.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
93
94/-- The CHSH combination of correlations.
95 S = E(a,b) - E(a,b') + E(a',b) + E(a',b') -/
96noncomputable def chshCombination (a a' b b' : MeasurementAngle) : ℝ :=
97 quantumCorrelation a b - quantumCorrelation a b' +
98 quantumCorrelation a' b + quantumCorrelation a' b'
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