def
definition
singlet
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Quantum.BellInequality on GitHub at line 69.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
66 correlationType : String
67
68/-- Create a singlet Bell pair: |ψ⟩ = (|01⟩ - |10⟩)/√2 -/
69def singlet (id : ℕ) : BellPair :=
70 ⟨id, trivial, "singlet"⟩
71
72/-! ## Quantum Correlations -/
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