Accepted Hardy settings agree

Proved

QAlgorithms.Papers.Independent.Intakethird100.P47.accepted_settings_agree

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $p(a,b\mid A,B)$ be a nonnegative binary conditional distribution normalized for each pair of settings, and let $w(A,B)$ be a nonnegative normalized input law. The joint law is $w(A,B)p(a,b\mid A,B)$ . Set $S=\{a=b=0\}$ , $s=\sum_{A,B}w(A,B)p(00\mid A,B)$ , and, when $s>0$ , let $J(A,B)=w(A,B)p(00\mid A,B)/s$ be the accepted setting law.

Assume $s>0$ and the two cross-setting zero constraints $p(00\mid10)=p(00\mid01)=0$ . Every unequal setting pair has zero joint acceptance mass, and

\Pr[A=B\mid S]=\sum_{A=B}J(A,B)=1.

This gives perfect agreement of the raw setting bits under the ideal cross-setting constraints.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P47

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P47

open scoped ComplexConjugate

open scoped BigOperators

/-- II B, PDF p.3, using (1) on p.2: accepted settings agree with probability one.
No restriction to qubits, uniform inputs or a claim of secrecy is involved. -/
theorem accepted_settings_agree (p : Behavior) (w : PairLaw)
    (hp : IsBehavior p) (hw : IsPairLaw w)
    (h10 : p true false false false = 0) (h01 : p false true false false = 0)
    (hs : 0 < siftingProbability p w) :
    (∀ A B, A ≠ B → acceptedMass p w A B = 0) ∧
    (∑ A, ∑ B, if A = B then acceptedLaw p w A B else 0) = 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P47

Source

Device-independent quantum key distribution based on measurement inputs, arXiv:1308.6447v3, PDF p. 3, II B: perfect correlation of accepted settings

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every function $p:\{0,1\}^4\to\mathbb R$ and function $w:\{0,1\}^2\to\mathbb R$ , where $0$ denotes false and $1$ true, assume $p(A,B,a,b)\ge0$ for every choice of its four arguments and $\sum_{a,b}p(A,B,a,b)=1$ for every $A,B$ ; assume also $w(A,B)\ge0$ for every pair and $\sum_{A,B}w(A,B)=1$ . If $p(1,0,0,0)=0$ , $p(0,1,0,0)=0$ , and

S=\sum_{A,B}w(A,B)p(A,B,0,0)>0,

then $w(A,B)p(A,B,0,0)=0$ for every $A\ne B$ , and

\sum_{A,B} \begin{cases} w(A,B)p(A,B,0,0)/S,&A=B,\\ 0,&A\ne B \end{cases} =1.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph