Scalar monotonicity at fixed Hardy statistics

Open

QAlgorithms.Papers.Independent.Intakethird100.P47.hardy_ratio_reduction

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 $w$ has full support, $h=H(p)$ where $H(p)=(p(00\mid00),-p(00\mid10),-p(00\mid01),-p(11\mid11))$ , $h_1>0$ , and $\sigma=\sum_Bw(0,B)p(00\mid0,B)>0$ . Then

\sigma=h_1w(00)-h_3w(01).

Every other normalized nonnegative behavior $p'$ with $H(p')=h$ has the same $\sigma$ and positive acceptance. Write $\nu=\sum_Bw(1,B)p(00\mid1,B)$ and similarly $\nu'$ for $p'$ . Then

\Pr_p[A=0\mid S]\le\Pr_{p'}[A=0\mid S]\iff \nu'\le\nu,

\Pr_p[A=1\mid S]\le\Pr_{p'}[A=1\mid S]\iff \nu\le\nu'.

Thus a feasible minimum of $\nu$ maximizes the first ratio and a feasible maximum maximizes the second. No existence or numerical certification of such endpoints is asserted.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P47

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P47

open scoped ComplexConjugate

open scoped BigOperators

/-- V, PDF p.7, using (12),(14)–(15) on pp.5–6: fixed Hardy data fix sigma.
The conditional zero ratio decreases with nu and the one ratio increases with nu.
Endpoints maximize the respective ratios when feasible endpoints exist; none are assumed attained. -/
theorem hardy_ratio_reduction (p : Behavior) (w : PairLaw)
    (hp : IsBehavior p) (hw : IsPairLaw w) (hwpos : ∀ A B, 0 < w A B)
    (hh1 : 0 < hardyStatistics p 0)
    (hsigma : 0 < aliceMass p w false) :
    aliceMass p w false = hardyStatistics p 0 * w false false -
      hardyStatistics p 2 * w false true ∧
    ∀ p2 : Behavior, IsBehavior p2 → hardyStatistics p2 = hardyStatistics p →
      aliceMass p2 w false = aliceMass p w false ∧
      0 < siftingProbability p2 w ∧
      (aliceMarginal (acceptedLaw p w) false ≤ aliceMarginal (acceptedLaw p2 w) false ↔
        aliceMass p2 w true ≤ aliceMass p w true) ∧
      (aliceMarginal (acceptedLaw p w) true ≤ aliceMarginal (acceptedLaw p2 w) true ↔
        aliceMass p w true ≤ aliceMass p2 w true) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P47

Source

Device-independent quantum key distribution based on measurement inputs, arXiv:1308.6447v3, PDF p. 7, V: scalar reduction for Hardy conditional ratios

Read-back

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

Identify the Boolean values false and true with $0$ and $1$ . Let $p_{AB}^{ab}$ be real numbers, nonnegative for all $A,B,a,b\in\{0,1\}$ , with $\sum_{a,b}p_{AB}^{ab}=1$ for every $A,B$ . Let $w_{AB}>0$ for every $A,B$ , with $\sum_{A,B}w_{AB}=1$ . For any such behavior $q$ , define its four statistics by $s(q)=(q_{00}^{00},-q_{10}^{00},-q_{01}^{00},-q_{11}^{11})$ , its masses by $m_A(q)=\sum_B w_{AB}q_{AB}^{00}$ , its total mass by $S(q)=\sum_{A,B}w_{AB}q_{AB}^{00}$ , and its normalized first-coordinate marginals by $a_A(q)=\sum_B w_{AB}q_{AB}^{00}/S(q)$ . Assume $s_0(p)>0$ and $m_0(p)>0$ . Then $m_0(p)=s_0(p)w_{00}-s_2(p)w_{01}$ . Furthermore, for every nonnegative normalized behavior $p_2$ with $s(p_2)=s(p)$ , all of the following hold:

m_0(p_2)=m_0(p),\qquad S(p_2)>0,

a_0(p)\le a_0(p_2)\ \Longleftrightarrow\ m_1(p_2)\le m_1(p), \qquad a_1(p)\le a_1(p_2)\ \Longleftrightarrow\ m_1(p)\le m_1(p_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