Balancing local setting bias and exact accepted yield

Open

QAlgorithms.Papers.Independent.Intakethird100.P47.balanced_input_bias_and_yield

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.

Let $x=p(00\mid00)>0$ , $y=p(00\mid11)>0$ , and assume both cross-setting acceptance probabilities vanish. Choose independent settings with $\Pr[A=0]=\Pr[B=0]=r\in[0,1]$ . Acceptance has positive probability even at the endpoints. With $r_b=\sqrt y/(\sqrt x+\sqrt y)\in(0,1)$ ,

\bigl(\forall k,\ \Pr[A=k\mid S]=\tfrac12\bigr) \iff xr^2=y(1-r)^2\iff r=r_b.

At this balancing bias,

s=2xr^2=\frac{2xy}{(\sqrt x+\sqrt y)^2}.

For $x=(5\sqrt5-11)/2$ and $y=\sqrt5-2$ , $r_b=(\sqrt5-1)/2$ . This balances the raw key values and evaluates acceptance; it does not maximize a specified cryptographic rate.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P47

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P47

open scoped ComplexConjugate

open scoped BigOperators

/-- VII B.2, PDF p.9, (19a,b): the unique equal local input bias balancing the ideal
accepted settings, with exact yield. The denominator is (sqrt(x)+sqrt(y)) squared.
The yield is a raw accepted-run probability, not an operational secrecy capacity. -/
theorem balanced_input_bias_and_yield (p : Behavior) (hp : IsBehavior p)
    (x y r : ℝ) (hx : 0 < x) (hy : 0 < y) (hr : 0 ≤ r ∧ r ≤ 1)
    (h00 : p false false false false = x) (h11 : p true true false false = y)
    (h10 : p true false false false = 0) (h01 : p false true false false = 0) :
    let w := binarySettingLaw r r
    let rb := Real.sqrt y / (Real.sqrt x + Real.sqrt y)
    0 < siftingProbability p w ∧ 0 < rb ∧ rb < 1 ∧
    ((∀ A, aliceMarginal (acceptedLaw p w) A = 1 / 2) ↔ x * r ^ 2 = y * (1 - r) ^ 2) ∧
    (x * r ^ 2 = y * (1 - r) ^ 2 ↔ r = rb) ∧
    (r = rb → siftingProbability p w = 2 * x * r ^ 2 ∧
      siftingProbability p w = 2 * x * y / (Real.sqrt x + Real.sqrt y) ^ 2) ∧
    (x = (5 * Real.sqrt 5 - 11) / 2 → y = Real.sqrt 5 - 2 →
      rb = (Real.sqrt 5 - 1) / 2) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P47

Source

Device-independent quantum key distribution based on measurement inputs, arXiv:1308.6447v3, PDF p. 9, VII B.2: balancing input distribution and exact ideal yield

Read-back

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

Identify false and true with $0$ and $1$ . Let $p_{AB}^{ab}\in\mathbb R$ be nonnegative for all $A,B,a,b\in\{0,1\}$ , with $\sum_{a,b}p_{AB}^{ab}=1$ for every $A,B$ . Let $x,y,r\in\mathbb R$ satisfy $x>0$ , $y>0$ , and $0\le r\le1$ , including the endpoints. Assume $p_{00}^{00}=x$ , $p_{11}^{00}=y$ , and $p_{10}^{00}=p_{01}^{00}=0$ . Put $q_0=r$ , $q_1=1-r$ , $w_{AB}=q_Aq_B$ , $S=\sum_{A,B}w_{AB}p_{AB}^{00}=xr^2+y(1-r)^2$ , $J_{AB}=w_{AB}p_{AB}^{00}/S$ , and $r_b=\sqrt y/(\sqrt x+\sqrt y)$ . Then $S>0$ , $0<r_b<1$ , and

\left(\forall A,\ \sum_B J_{AB}=\frac12\right) \Longleftrightarrow xr^2=y(1-r)^2, \qquad xr^2=y(1-r)^2\Longleftrightarrow r=r_b.

If $r=r_b$ , then $S=2xr^2$ and $S=2xy/(\sqrt x+\sqrt y)^2$ . If additionally $x=(5\sqrt5-11)/2$ and $y=\sqrt5-2$ , then $r_b=(\sqrt5-1)/2$ .

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