Nonuniform private inputs have lower entropy cost

Proved

QAlgorithms.Papers.Independent.Intakethird100.P47.nonuniform_input_entropy

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

prove2quantum

Let $A$ and $B$ be independent private binary settings, each with probability $r\in[0,1]$ of input zero. Let $h_2(r)=-r\log_2r-(1-r)\log_2(1-r)$ , with $0\log 0=0$ , and let $H(A,B)$ be Shannon entropy in bits. Then

H(A,B)=2h_2(r),\qquad r\ne\tfrac12\ \Longrightarrow\ H(A,B)<2.

In particular $r_*=(\sqrt5-1)/2$ lies strictly between zero and one and has $H(A,B)<2$ . This is the asymptotic Shannon randomness cost of the independent input source, not a finite-seed length or a security statement for correlated adversarial randomness.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P47

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P47

open scoped ComplexConjugate

open scoped BigOperators

/-- IV B / VII A, PDF pp.6,8–9: nonuniform independent private settings cost less
Shannon entropy than two fair bits; the ideal chosen bias is included explicitly.
This is a population entropy statement, not an exact finite random-seed length. -/
theorem nonuniform_input_entropy :
    (∀ r : ℝ, 0 ≤ r → r ≤ 1 →
      pairEntropy (binarySettingLaw r r) = 2 * binEntropy2 r ∧
      (r ≠ 1 / 2 → pairEntropy (binarySettingLaw r r) < 2)) ∧
    (0 < (Real.sqrt 5 - 1) / 2 ∧ (Real.sqrt 5 - 1) / 2 < 1) ∧
    pairEntropy (binarySettingLaw ((Real.sqrt 5 - 1) / 2) ((Real.sqrt 5 - 1) / 2)) < 2 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P47

Source

Device-independent quantum key distribution based on measurement inputs, arXiv:1308.6447v3, PDF p. 6, IV B / VII A: nonuniform inputs require less randomness

Read-back

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

For $r\in[0,1]$ , define $q_0=r$ , $q_1=1-r$ , and the pair law $w^{(r)}_{AB}=q_Aq_B$ on $A,B\in\{0,1\}$ . For a pair law $j$ , write $H(j)=-\sum_{A,B}j_{AB}\log(j_{AB})/\log2$ , where $\log$ is the natural logarithm and a zero entry contributes zero. Write $h_2(r)=[-r\log r-(1-r)\log(1-r)]/\log2$ , with the same zero-term convention. The declaration asserts the conjunction of these claims: for every real $r$ with $0\le r\le1$ , including $r=0$ and $r=1$ ,

H(w^{(r)})=2h_2(r), \qquad r\ne\frac12\ \Longrightarrow\ H(w^{(r)})<2;

the number $g=(\sqrt5-1)/2$ satisfies $0<g<1$ ; and $H(w^{(g)})<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