Documentation

CsdLean4.Empirical.QM.Crypto.E91

Empirical: E91 device-independent certification — the local-hidden-variable CHSH bound #

Category: 3-Local. The LHV CHSH ≤ 2 bound is QM-generic (a theorem about a hidden-variable probability space, no CSD ontology) and promotion-ready to 2-Framework; the QM tie-in re-uses Bell.lean's Tsirelson saturation.

Scope (honest). What is proved is the correlation-level certification: the singlet attains 2√2 while every LHV model is ≤ 2, so no local-realistic description reproduces the quantum correlations (the basis of E91's eavesdropper-detection). This is not a full cryptographic security proof — there is no key-rate, finite-key, or general-adversary analysis here. "Device-independent" refers to the certification being LHV-model-agnostic, not to a security theorem.

What this closes #

Empirical/QM/Bell.lean carries bellClassicalBoundValue : ℝ := 2 as a named constant, explicitly not a theorem that any local-hidden-variable (LHV) model satisfies |S| ≤ 2 (see its docstring). This file supplies that missing theorem, turning the Bell-1964 classical bound into genuine Lean content and giving the device-independent (Ekert 1991) security witness real teeth:

The mathematics #

The LHV model is the standard one: a probability space (Λ, μ) of hidden variables and deterministic ±1 response functions, with factorisable correlations E(a,b) = ∫ A(a,λ) B(b,λ) dμ(λ). The bound is the pointwise Bell–CHSH algebra

S(λ) = A(a,λ)B(b,λ) − A(a,λ)B(b',λ) + A(a',λ)B(b,λ) + A(a',λ)B(b',λ) ∈ {−2, +2},

so |S(λ)| ≤ 2 for every λ (a 16-way ±1 case split), followed by integral monotonicity |∫ S dμ| ≤ ∫ |S| dμ ≤ ∫ 2 dμ = 2 on the probability measure μ. This is Bell's 1964 inequality in the CHSH (Clauser–Horne–Shimony–Holt 1969) form; the integrand bound is the whole content, the rest is monotonicity of the Bochner integral.

Experimental verification #

The factorisable LHV correlation #

source
noncomputable def CSD.Empirical.QM.E91.lhvCorrelation {Λ : Type u_1} [MeasurableSpace Λ] {SettingA : Type u_2} {SettingB : Type u_3} (μ : MeasureTheory.Measure Λ) (A : SettingA → Λ → ℝ) (B : SettingB → Λ → ℝ) (a : SettingA) (b : SettingB) :
ℝ

The local-hidden-variable correlation E(a,b) = ∫ A(a,λ)·B(b,λ) dμ(λ): the expectation of the product of the two sides' local ±1 responses, the only correlation a local-hidden-variable model can produce.

Equations
Instances For
    source
    noncomputable def CSD.Empirical.QM.E91.lhvCHSH {Λ : Type u_1} [MeasurableSpace Λ] {SettingA : Type u_2} {SettingB : Type u_3} (μ : MeasureTheory.Measure Λ) (A : SettingA → Λ → ℝ) (B : SettingB → Λ → ℝ) (a a' : SettingA) (b b' : SettingB) :
    ℝ

    The CHSH combination of four LHV correlations, S = E(a,b) − E(a,b') + E(a',b) + E(a',b').

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      The Bell/CHSH inequality |S| ≤ 2 #

      source
      theorem CSD.Empirical.QM.E91.lhvCHSH_abs_le_two {Λ : Type u_1} [MeasurableSpace Λ] {SettingA : Type u_2} {SettingB : Type u_3} (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A : SettingA → Λ → ℝ) (B : SettingB → Λ → ℝ) (hA : ∀ (a : SettingA), Measurable (A a)) (hB : ∀ (b : SettingB), Measurable (B b)) (hApm : ∀ (a : SettingA) (l : Λ), A a l = 1 ∨ A a l = -1) (hBpm : ∀ (b : SettingB) (l : Λ), B b l = 1 ∨ B b l = -1) (a a' : SettingA) (b b' : SettingB) :
      |lhvCHSH μ A B a a' b b'| ≤ 2

      The Bell–CHSH inequality for any local-hidden-variable model. For a hidden-variable probability space (Λ, μ) and ±1-valued, measurable local response functions A, B, the CHSH combination of the factorisable correlations satisfies |S| ≤ 2.

      Bell 1964 (Physics 1, 195) in the CHSH 1969 form. The proof is the pointwise ±1 identity S(λ) ∈ {−2, +2} plus monotonicity of the Bochner integral on the probability measure μ.

      Strict separation from the quantum Tsirelson value #

      source
      theorem CSD.Empirical.QM.E91.lhvCHSH_lt_tsirelson {Λ : Type u_1} [MeasurableSpace Λ] {SettingA : Type u_2} {SettingB : Type u_3} (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A : SettingA → Λ → ℝ) (B : SettingB → Λ → ℝ) (hA : ∀ (a : SettingA), Measurable (A a)) (hB : ∀ (b : SettingB), Measurable (B b)) (hApm : ∀ (a : SettingA) (l : Λ), A a l = 1 ∨ A a l = -1) (hBpm : ∀ (b : SettingB) (l : Λ), B b l = 1 ∨ B b l = -1) (a a' : SettingA) (b b' : SettingB) :
      lhvCHSH μ A B a a' b b' < 2 * √2

      Every LHV CHSH value is strictly below the quantum Tsirelson bound 2√2.

      E91 device-independent security witness #

      source
      theorem CSD.Empirical.QM.E91.e91_no_lhv_reproduces_singlet :
      (∃ (a : LF3.DetectorSetting) (a' : LF3.DetectorSetting) (b : LF3.DetectorSetting) (b' : LF3.DetectorSetting), |Bell.chshOperator a a' b b'| = 2 * √2) ∧ ∀ {Λ : Type u_4} [inst : MeasurableSpace Λ] {SettingA : Type u_5} {SettingB : Type u_6} (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A : SettingA → Λ → ℝ) (B : SettingB → Λ → ℝ), (∀ (a : SettingA), Measurable (A a)) → (∀ (b : SettingB), Measurable (B b)) → (∀ (a : SettingA) (l : Λ), A a l = 1 ∨ A a l = -1) → (∀ (b : SettingB) (l : Λ), B b l = 1 ∨ B b l = -1) → ∀ (xa xa' : SettingA) (xb xb' : SettingB), |lhvCHSH μ A B xa xa' xb xb'| ≤ 2

      E91 device-independent security witness. The singlet at canonical angles realises a CHSH magnitude of 2√2 (Bell A1, chsh_singlet_tsirelson_bound), while every local-hidden-variable model — any hidden-variable probability space with ±1 local responses — is capped at |S| ≤ 2. Since 2 < 2√2, an observed CHSH value at the Tsirelson bound is unreproducible by any LHV model, hence certifies the absence of any local-realistic (eavesdropper) description of the source. This is the device-independent security guarantee underlying the Ekert 1991 protocol.

      Experimental verification: Ekert 1991, Phys. Rev. Lett. 67, 661; loophole-free Bell tests: Hensen 2015, Giustina 2015, Shalm 2015.