Prove2Me

∣μa∣≤5M8−Nr|\mu_{\mathbf a}|\le 5^M8^{-N_r} (corrected: Γa\Gamma_{\mathbf a} from transposed tables)

Proved
NoSignalPA.abs_mu_le

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

cryptographynonlocalityp2o-correctedp2o-gran-per-chapterp2o-plan-paperp2o-v1privacy-amplificationquantum-information

Fix an entry (a0,b0,x0,y0)(\mathbf a_0,\mathbf b_0,\mathbf x_0,\mathbf y_0) and let M=∥a0⊕b0⊕x0⋅y0∥M=\|\mathbf a_0\oplus\mathbf b_0\oplus\mathbf x_0\cdot\mathbf y_0\|. For every string a\mathbf a, the coefficient μa=Γa(a0,b0,x0,y0)\mu_{\mathbf a}=\Gamma_{\mathbf a}(\mathbf a_0,\mathbf b_0,\mathbf x_0,\mathbf y_0) satisfies

∣μa∣≤5M 8−Nr.|\mu_{\mathbf a}|\le 5^M\,8^{-N_r}.

This is the uniform bound on the weights that makes the exponential-moment argument of Lemma 2 applicable.

Differences from the source:

  • correction: |Γ_a⟩ built from the tables |γ₀⟩, |γ₁⟩ printed in Lemma 1 (p. 2) → |Γ_a⟩ built from their transposes (gammaCoef); reason: the printed tables are transposed relative to layout (3): for Nr = 1 and the nonsignaling box a = 1 ⊕ x, b = 0, P_{a=0|x=0} = 0 but the printed ⟨γ₀|P⟩ = 1; with the transposes Lemma 1 holds; this statement is unchanged by the transposition, because a ⊕ b ⊕ x·y is symmetric under (a, x) ↔ (b, y)
Preamble
import Mathlib
import Definitions.Def_NoSignalPA_gammaVec
import Definitions.Def_NoSignalPA_ones
Formal statement
namespace NoSignalPA

/-- **`|μ_a| ≤ 5^M 8^{−Nr}`.**
Ll. Masanes, *Universally-composable privacy amplification from causality constraints*,
arXiv:0807.2158v4, Appendix, proof of Lemma 2, p. 5 (PDF p. 5): "Let `µ_a = Γ_a(a0, b0, x0, y0)`,
`M = ‖a0 ⊕ b0 ⊕ x0 · y0‖`, and note that `|µ_a| ≤ 5^M 8^{−Nr}` for all a."

For a fixed entry `(a₀, b₀, x₀, y₀)` and every string `s` (the paper's `a`),
`|Γ_s(a₀, b₀, x₀, y₀)| ≤ 5^M · 8^{−Nr}` with `M = ‖a₀ ⊕ b₀ ⊕ x₀·y₀‖`.

**Formalization Note.** `Γ_s` is the corrected vector (transposed tables); the bound holds for
the printed tables too, since `a ⊕ b ⊕ x·y` is symmetric under `(a, x) ↔ (b, y)`. -/
theorem abs_mu_le {Nr : ℕ} (s a₀ b₀ x₀ y₀ : Str Nr) :
    |gammaVec s a₀ b₀ x₀ y₀|
      ≤ 5 ^ ones (fun i => xor (xor (a₀ i) (b₀ i)) (x₀ i && y₀ i)) * ((8 : ℝ) ^ Nr)⁻¹ := by sorry

end NoSignalPA
Source
Masanes, Universally-composable privacy amplification from causality constraints, arXiv:0807.2158v4, Appendix, proof of Lemma 2, p.5
Human review

  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph