quantumCorrelation

formal source

  73
  74/-- Quantum correlation function for singlet state.
  75    E(a,b) = -cos(a - b) -/
  76noncomputable def quantumCorrelation (a b : MeasurementAngle) : ℝ :=
  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