Equal weights are forced for four signed biases

Proved

QAlgorithms.Papers.Independent.Intakethird100.P47.signed_bias_equal_weights

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

prove2quantum

Let $0<p_A,p_B<1$ and $0<\epsilon\le\min(p_A,1-p_A,p_B,1-p_B)$ . For $e=(e_A,e_B)\in\{-1,+1\}^2$ , let $w_e$ be the independent binary setting law with probabilities of input zero $p_A+e_A\epsilon$ and $p_B+e_B\epsilon$ . Let $w$ be the product law with parameters $p_A,p_B$ , and let $t_e\ge0$ sum to one. Then

\bigl(\forall A,B,\ \sum_e t_e w_e(A,B)=w(A,B)\bigr) \quad\Longleftrightarrow\quad \forall e,\ t_e=\tfrac14.

This is uniqueness of the prior mixture producing the nominal input distribution. It does not give the bias-label distribution after acceptance.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P47

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P47

open scoped ComplexConjugate

open scoped BigOperators

/-- III, PDF p.4: the four signed-bias mixture equals (5) exactly for equal weights.
The necessary exclusion epsilon=0 is explicit; endpoint component probabilities may be zero. -/
theorem signed_bias_equal_weights (pA pB epsilon : ℝ)
    (hA : 0 < pA ∧ pA < 1) (hB : 0 < pB ∧ pB < 1)
    (he : 0 < epsilon)
    (heA : epsilon ≤ pA ∧ epsilon ≤ 1 - pA)
    (heB : epsilon ≤ pB ∧ epsilon ≤ 1 - pB)
    (t : (Bool × Bool) → ℝ) (ht : ∀ e, 0 ≤ t e) (hsum : ∑ e, t e = 1) :
    ((∀ A B, (∑ e, t e * biasedInput pA pB epsilon e A B) = binarySettingLaw pA pB A B) ↔
      ∀ e, t e = 1 / 4) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P47

Source

Device-independent quantum key distribution based on measurement inputs, arXiv:1308.6447v3, PDF p. 4, III: equal weights of four signed biases

Read-back

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

For all real $p_A,p_B,\epsilon$ satisfying $0<p_A<1$ , $0<p_B<1$ , $\epsilon>0$ , $\epsilon\le p_A$ , $\epsilon\le1-p_A$ , $\epsilon\le p_B$ , and $\epsilon\le1-p_B$ , and every function $t:\{0,1\}^2\to\mathbb R$ satisfying $t(e)\ge0$ for every $e$ and $\sum_e t(e)=1$ , the following equivalence holds. Write $0$ for false and $1$ for true, define $s(0)=-1$ , $s(1)=1$ , and define $b(r,0)=r$ , $b(r,1)=1-r$ . Then

\left[ \forall A,B\in\{0,1\},\ \sum_{e\in\{0,1\}^2}t(e)\, b(p_A+s(e_1)\epsilon,A)\, b(p_B+s(e_2)\epsilon,B) =b(p_A,A)b(p_B,B) \right] \iff \left[\forall e\in\{0,1\}^2,\ t(e)=\frac14\right].

The non-strict upper bounds on $\epsilon$ permit shifted parameters to equal $0$ or $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