quantum_correlation_bounded

formal source

  77  -Real.cos (a - b)
  78
  79/-- **THEOREM**: Quantum correlation is bounded by 1. -/
  80theorem quantum_correlation_bounded (a b : MeasurementAngle) :
  81    |quantumCorrelation a b| ≤ 1 := by
  82  unfold quantumCorrelation
  83  simp only [abs_neg]
  84  exact abs_cos_le_one _
  85
  86/-- **THEOREM**: Perfect anticorrelation when measuring same direction. -/
  87theorem perfect_anticorrelation (a : MeasurementAngle) :
  88    quantumCorrelation a a = -1 := by
  89  unfold quantumCorrelation
  90  simp
  91
  92/-! ## Classical (Hidden Variable) Bounds -/
  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