Public-coin pointer-endpoint upper bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P81.pointer_endpoint_public_upper

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

prove2quantum

For $n\ge2$ and $k\ge1$ , let $g_k$ be the vertex reached after $k+1$ alternating applications of unrestricted pointer maps, beginning at a fixed Alice vertex $v_1$ . Messages alternate starting with Bob, and the final receiver may locally announce the endpoint without a further charged message. Use public randomness independent of both inputs, and require success at least $1-\varepsilon$ on every pair of maps, where $0<\varepsilon<1$ .

There are absolute constants $C>0,n_0\ge2$ , chosen before all these parameters, such that for $n\ge n_0$ a protocol with at most $k$ messages has worst-case bit cost $c$ satisfying

c\le C\left[\frac{n}{k\varepsilon}\left(L_{\lfloor k/2\rfloor}(n)+\log_2 k\right)+k\log_2 n\right].

Here $L_0(n)=\max\{1,n\}$ and $L_{j+1}(n)=\max\{1,\log_2 L_j(n)\}$ : the superscript denotes iteration, and precision saturates at one bit.

This is the stronger vertex-valued bound, rather than a bound only for pointer parity. Integer round-pair and bit-rounding conventions are absorbed in the absolute constant.

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 2, PDF p.13: public-coin endpoint bound, floor(k/2) iterates and one-bit saturation.
Odd k extends the preceding even case by one pointer message; k=1 can send the full table. -/
theorem pointer_endpoint_public_upper :
    ∃ C : ℝ, 0 < C ∧ ∃ n0 : ℕ, 2 ≤ n0 ∧
      ∀ (k n : ℕ), 0 < k → n0 ≤ n → ∀ eps : ℝ, 0 < eps → eps < 1 →
      ∀ v1 : Fin n, ∃ (c : ℕ) (P : PublicProtocol (PointerMap n) (PointerMap n) (Vertex n)),
        P.bounded .bob k c ∧ P.computes (endpoint k v1) eps ∧
        (c : ℝ) ≤ C * ((n : ℝ) / ((k : ℝ) * eps) *
          (iteratedLog (k / 2) n + Real.logb 2 k) + k * Real.logb 2 n) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P81

end

Source

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

Read-back

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

There exist a real constant $C>0$ and a natural number $n_0\geq2$ such that, for all natural numbers $k,n$ with $k>0$ and $n\geq n_0$ , every real $0<\varepsilon<1$ , and every $v_1\in\{0,\ldots,n-1\}$ , there exist a natural number $c$ and a public-randomness classical protocol $P$ with inputs $a,b:\{0,\ldots,n-1\}\to\{0,\ldots,n-1\}$ and output in the disjoint union $\{L(v)\}\sqcup\{R(v)\}$ satisfying the following properties. Such a protocol consists of finitely many deterministic binary communication trees with nonnegative seed weights summing to $1$ ; an internal node transmits a Boolean function of the speaking party's own input, and a leaf outputs a function of either party's own input. For every seed of positive weight, every root-to-leaf path has at most $c$ transmitted bits, and its number of maximal consecutive blocks of transmissions by the same party, plus one if its first sender is Alice, is at most $k$ ; a path with no transmissions has round count $0$ . For every $a,b$ , the total seed weight of trees outputting the result of exactly $k+1$ applications of $L(v)\mapsto R(a(v))$ , $R(v)\mapsto L(b(v))$ , starting at $L(v_1)$ , is at least $1-\varepsilon$ . Moreover,

c\leq C\left[ \frac{n}{k\varepsilon} \left(\Lambda_{\lfloor k/2\rfloor}(n)+\log_2 k\right) +k\log_2 n \right], \qquad \Lambda_0(x)=\max(1,x),\quad \Lambda_{j+1}(x)=\max\!\left(1,\log_2\Lambda_j(x)\right).

The division $k/2$ in the iteration index is natural-number division, hence rounds down. The constants $C,n_0$ are independent of $k,n,\varepsilon,v_1$ ; bounds on trees apply only to seeds of positive weight.

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