Fixed-round quantum non-disjointness lower bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P81.bounded_round_non_disjointness_lower

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

prove2quantum

Fix an integer $k\ge1$ independently of the input length. Alice and Bob receive $x,y\in\{0,1\}^n$ and must output one exactly when some coordinate has $x_i=y_i=1$ . A quantum protocol may start with any finite normalized, input-independent prior entangled state, use arbitrary private workspace, and exchange $k$ alternating messages starting with either player. It must succeed with probability at least $2/3$ on every input; only transmitted qubits are charged.

There are constants $C_k>0$ and $n_k\ge2$ such that for all $n\ge n_k$ , every such protocol has cost

c\ge C_k n^{1/k}.

The constants may depend on the fixed round count. This is the paper's non-disjointness output convention despite its notation $\mathrm{DISJ}_n$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P81

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable

namespace QAlgorithms.Papers.Independent.Intakethird100.P81

open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntropyBits)

open QAlgorithms.Papers.Independent.Bridge50.P44 (ClassicalFirst)

/-- Theorem 4, PDF p.19: k is fixed before the positive constant and eventual threshold.
Either starter is allowed; DISJ has the source's non-disjointness output convention. -/
theorem bounded_round_non_disjointness_lower (k : ℕ) (hk : 0 < k) :
    ∃ C : ℝ, 0 < C ∧ ∃ n0 : ℕ, 2 ≤ n0 ∧ ∀ n : ℕ, n0 ≤ n →
      ∀ (start : Party) (P : QuantumProtocol (Fin n → Bool) (Fin n → Bool) Bool),
        P.valid start k → P.computes nonDisjoint (1 / 3) →
        C * (n : ℝ) ^ (1 / (k : ℝ)) ≤ P.cost := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P81

end

Source

On rounds in quantum communication, arXiv:quant-ph/0004100v5, PDF p. 19, Theorem 4

Read-back

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

For every natural number $k>0$ , there exist a real constant $C>0$ and a natural number $n_0\geq2$ such that, for every natural number $n\geq n_0$ , either starting party, and every Boolean-output quantum protocol $P$ on inputs $x,y:\{0,\ldots,n-1\}\to\{\mathrm{false},\mathrm{true}\}$ , the following implication holds. Suppose $P$ 's initial vector has norm $1$ , its round list has length exactly $k$ , speakers alternate beginning with the specified starting party, and each round applies its speaker's own-input-dependent unitary within that speaker's currently owned wires and sends only currently owned wires to the other party. Suppose further that, for every input pair, the designated output party's own-input-dependent Boolean measurement consists of positive semidefinite matrices summing to the identity and acting within that party's final owned wires. Acting within a wire set means being an arbitrary matrix on some injectively selected wires in that set tensored with the identity on all others, allowing zero selected wires. If, for every $x,y$ , the probability of outputting $\mathrm{true}$ exactly when there exists $i$ with $x(i)=y(i)=\mathrm{true}$ is at least $2/3$ , where outcome probabilities are real traces against the final pure-state matrix obtained by applying all round unitaries, then

C\,n^{1/k}\leq \sum_{r\text{ in }P}|r.\mathrm{sent}|.

The exponent $1/k$ is real division. The constants may depend on $k$ , but are common to all subsequent $n$ , starting parties, and protocols; empty sent sets are allowed.

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