Empirical/QM: E91 finite-sample (finite-key) concentration

Category: 3-Local (QM-validity content, no CSD ontology).

The asymptotic key rate E91.e91_key_rate_pos_of_chsh takes the true CHSH value S as given. A real device-independent QKD run does not see S; it estimates it from n finite rounds. This module supplies the missing finite-sample bridge: the empirical CHSH estimator Ŝₙ concentrates around the true S exponentially in n, so the probability of failing to certify a genuine violation decays like exp(−n ε² / (2c)).

Model (minimal and honest)

A run is a sequence of per-round CHSH statistics Y : ℕ → Ω → ℝ. Each round's statistic is

• bounded: Y i ω ∈ [a, b] almost surely (a ≤ b); the width b − a is the range of the per-round CHSH correlator combination (modelling choice — e.g. the standard randomized-setting unbiased per-round estimator lands in a fixed bounded interval). The Hoeffding constant is c = ((b − a)/2)²;
• unbiased: μ[Y i] = S (the true CHSH value);
• independent: iIndepFun Y μ (the per-round independence is a modelling hypothesis, exactly the i.i.d.-rounds assumption; it is what the sub-Gaussian add/sum API consumes — the same independence idiom LF1 threads).

Ŝₙ = (∑_{i<n} Yᵢ) / n is the empirical CHSH estimator (empiricalCHSH).

What this delivers

• e91_chsh_concentration — the headline: a genuine Hoeffding tail, μ.real {ω | Ŝₙ ω ≤ S − ε} ≤ exp(−n ε² / (2·((b−a)/2)²)), proved through Mathlib's sub-Gaussian pipeline (Hoeffding's lemma hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero per round, summed with measure_sum_range_ge_le_of_iIndepFun, the Chernoff measure_ge_le tail). The exponent genuinely decays in n (linear in n, constant c = ((b−a)/2)² > 0 whenever a < b).
• e91_finite_key_confidence — the bridge: for a true violation 2 < S ≤ 2√2, (1) the asymptotic rate is positive (e91_key_rate_pos_of_chsh), (2) the failure-to-certify probability μ.real {ω | Ŝₙ ω ≤ 2} is ≤ exp(−n (S−2)²/(2·((b−a)/2)²)), and (3) the estimator certifies (2 < Ŝₙ) with probability ≥ 1 − exp(−n (S−2)²/…). The failure probability is exponentially small in the number of rounds.

Honest scope

This is finite-sample confidence: Hoeffding concentration of the CHSH estimator. It is not a composable finite-key security proof. A full finite-key analysis (Renner smooth min-entropy, the leftover-hash / privacy- amplification accounting, the entropy-accumulation theorem) needs infrastructure Mathlib does not have; none of it is claimed here. The per-round independence and boundedness are explicit modelling hypotheses (not derived). QM-validity inner-product layer; no CSD ontology. Foundational triple only (no busch).

Source

Hoeffding 1963; Pironio et al. 2009 (DIQKD finite-key); Tomamichel–Lim– Gisin–Renner 2012 (composable finite-key, not formalised here).

noncomputable def CSD.Empirical.QM.E91.empiricalCHSH {Ω : Type u_1} (Y : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ

The empirical CHSH estimator over n rounds: the sample mean of the per-round CHSH statistics Y, Ŝₙ(ω) = (∑_{i<n} Yᵢ ω) / n.

Equations

• CSD.Empirical.QM.E91.empiricalCHSH Y n ω = (∑ i ∈ Finset.range n, Y i ω) / ↑n

theorem CSD.Empirical.QM.E91.e91_chsh_concentration {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : ℕ → Ω → ℝ} {S a b : ℝ} {n : ℕ} (hn : 0 < n) (hab : a ≤ b) (hmeas : ∀ (i : ℕ), Measurable (Y i)) (hindep : ProbabilityTheory.iIndepFun Y μ) (hbound : ∀ (i : ℕ), ∀ᵐ (ω : Ω) ∂μ, Y i ω ∈ Set.Icc a b) (hmean : ∀ (i : ℕ), ∫ (x : Ω), Y i x ∂μ = S) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω : Ω | empiricalCHSH Y n ω ≤ S - ε} ≤ Real.exp (-↑n * ε ^ 2 / (2 * ((b - a) / 2) ^ 2))

E91 finite-sample CHSH concentration (Hoeffding tail). For n bounded (Y i ∈ [a,b] a.s.), unbiased (μ[Y i] = S), independent (iIndepFun Y μ) per-round CHSH statistics, the empirical estimator Ŝₙ deviates below the true value S by ε ≥ 0 with exponentially small probability:

μ.real {ω | Ŝₙ ω ≤ S − ε} ≤ exp(−n ε² / (2·((b−a)/2)²)).

The Hoeffding constant is c = ((b−a)/2)² (the per-round sub-Gaussian parameter). The exponent is linear in n and strictly negative for ε > 0, a < b, so the bound genuinely decays. Proved by Hoeffding's lemma (hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero, per round, on the centered variable S − Y i) + the i.i.d. sub-Gaussian Hoeffding sum (measure_sum_range_ge_le_of_iIndepFun, which is the Chernoff measure_ge_le tail of the summed sub-Gaussian).

theorem CSD.Empirical.QM.E91.e91_finite_key_confidence {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : ℕ → Ω → ℝ} {S a b : ℝ} {n : ℕ} (hn : 0 < n) (hab : a ≤ b) (hmeas : ∀ (i : ℕ), Measurable (Y i)) (hindep : ProbabilityTheory.iIndepFun Y μ) (hbound : ∀ (i : ℕ), ∀ᵐ (ω : Ω) ∂μ, Y i ω ∈ Set.Icc a b) (hmean : ∀ (i : ℕ), ∫ (x : Ω), Y i x ∂μ = S) (hS : 2 < S) (hS' : S ≤ 2 * √2) : 0 < e91KeyRate S ∧ μ.real {ω : Ω | empiricalCHSH Y n ω ≤ 2} ≤ Real.exp (-↑n * (S - 2) ^ 2 / (2 * ((b - a) / 2) ^ 2)) ∧ 1 - Real.exp (-↑n * (S - 2) ^ 2 / (2 * ((b - a) / 2) ^ 2)) ≤ μ.real {ω : Ω | 2 < empiricalCHSH Y n ω}

E91 finite-key confidence (the bridge). For a true CHSH violation 2 < S ≤ 2√2 certified by independent, bounded, unbiased per-round statistics:

1. the asymptotic DI secret-key rate is strictly positive (e91_key_rate_pos_of_chsh);
2. the failure-to-certify probability — the empirical estimator landing at or below the classical ceiling 2 — is exponentially small in n, μ.real {ω | Ŝₙ ω ≤ 2} ≤ exp(−n (S−2)² / (2·((b−a)/2)²));
3. equivalently, the estimator certifies (2 < Ŝₙ) with probability ≥ 1 − exp(−n (S−2)² / (2·((b−a)/2)²)).

This is the finite-round content: the asymptotic positive key rate plus a finite-sample confidence that the estimate witnesses the violation. It is not composable finite-key security (no smooth min-entropy / leftover hashing); see the module docstring.