Prove2Me

For a uniformly random hh, the indicators Va=[h(a)=k]V_{\mathbf a}=[h(\mathbf a)=\mathbf k] are independent with Pr⁡{Va=1}=2−Ns\Pr\{V_{\mathbf a}=1\}=2^{-N_s}

Proved
NoSignalPA.preimage_indicators

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

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

Fix k∈{0,1}Ns\mathbf k\in\{0,1\}^{N_s} and pick h:{0,1}Nr→{0,1}Nsh:\{0,1\}^{N_r}\to\{0,1\}^{N_s} uniformly at random. Let Va=1V_{\mathbf a}=1 if h(a)=kh(\mathbf a)=\mathbf k (that is, a∈Ak\mathbf a\in\mathcal A_{\mathbf k}) and Va=0V_{\mathbf a}=0 otherwise. Then for every finite set SS of strings and every prescribed pattern (va)a∈S(v_{\mathbf a})_{\mathbf a\in S} of bits,

Pr⁡{Va=va for all a∈S}=∏a∈Sq(va),q(1)=2−Ns, q(0)=1−2−Ns.\Pr\{V_{\mathbf a}=v_{\mathbf a}\ \text{for all }\mathbf a\in S\}=\prod_{\mathbf a\in S}q(v_{\mathbf a}),\qquad q(1)=2^{-N_s},\ q(0)=1-2^{-N_s}.

That is, the VaV_{\mathbf a} are independent and Pr⁡{Va=1}=2−Ns\Pr\{V_{\mathbf a}=1\}=2^{-N_s} for all a\mathbf a.

Differences from the source:

  • encoding: the random variables V_a are independent and Prob{V_a = 1} = 2^{−Ns} → the joint law of every finite subfamily (V_a)_{a∈S} factorizes with marginals 2^{−Ns}, 1 − 2^{−Ns}; V_a is the Boolean [h(a) = k]; reason: for finitely many Bernoulli variables this factorization is the definition of independence with these marginals
Preamble
import Mathlib
import Definitions.Def_NoSignalPA_Str
import Definitions.Def_OAI_Probability_ThorpCompatibility_PermutationProbability
Formal statement
namespace NoSignalPA

/-- **For a uniformly random `h`, the indicators `V_a = [h(a) = k]` are independent with
`Prob{V_a = 1} = 2^{−Ns}`.**
Ll. Masanes, *Universally-composable privacy amplification from causality constraints*,
arXiv:0807.2158v4, Appendix, proof of Lemma 2, p. 5 (PDF p. 5): "Let `V_a = 1` if the string a belongs to
`A_k`, and `V_a = 0` otherwise. If we pick a random function h with uniform distribution over the
set of all functions, then the random variables `V_a` are independent and distributed according
to `Prob{V_a = 1} = 2^{−Ns}`, for all a."

For every key `k`, every finite set `S` of strings and every prescribed pattern `v`, the
probability that `V_a = v(a)` for all `a ∈ S` is `∏_{a∈S} q(v(a))`, with `q(1) = 2^{−Ns}`,
`q(0) = 1 − 2^{−Ns}`.

**Formalization Note.** `V_a` is the Boolean `decide (h a = k)`. Independence with these
marginals is stated as the factorization of the joint law of every subfamily
`(V_a)_{a∈S}`; `S = {a}` gives `Prob{V_a = 1} = 2^{−Ns}`. -/
theorem preimage_indicators {Nr Ns : ℕ} (k : Str Ns) (S : Finset (Str Nr))
    (v : Str Nr → Bool) :
    OAI.ThorpCompatibility.uniformProbability (fun h : Str Nr → Str Ns => ∀ a ∈ S, decide (h a = k) = v a)
      = ∏ a ∈ S, (if v a then ((2 : ℝ) ^ Ns)⁻¹ else 1 - ((2 : ℝ) ^ Ns)⁻¹) := 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