Iterated-logarithmic round upper bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P81.pointer_endpoint_logstar_upper

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

prove2quantum

Let $g_k$ be the same unrestricted pointer endpoint function on $n$ vertices per side. Write $\log_2^* n$ for the least $j$ with $L_j(n)\le1$ , where $L_0(n)=\max\{1,n\}$ and $L_{j+1}(n)=\max\{1,\log_2 L_j(n)\}$ . There are absolute $C>0,n_0\ge2$ such that whenever $n\ge n_0$ , $k\ge1$ and $k\ge2\log_2^* n$ , there is a public-coin, Bob-starting protocol using at most $k$ messages, correct with probability at least $2/3$ on every input, whose worst-case bit cost satisfies

c\le C\left(\frac{n}{k}+k\right)\log_2 k.

The fixed starting vertex is chosen independently of the inputs, and the final local announcement is uncharged. This keeps both resource terms and makes the iterated-logarithm threshold explicit.

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)

/-- Corollary 1, PDF p.13: both n/k and k are retained, with fixed error 1/3. -/
theorem pointer_endpoint_logstar_upper :
    ∃ C : ℝ, 0 < C ∧ ∃ n0 : ℕ, 2 ≤ n0 ∧
      ∀ (k n : ℕ), 0 < k → n0 ≤ n → 2 * logStar n ≤ k →
      ∀ v1 : Fin n, ∃ (c : ℕ) (P : PublicProtocol (PointerMap n) (PointerMap n) (Vertex n)),
        P.bounded .bob k c ∧ P.computes (endpoint k v1) (1 / 3) ∧
        (c : ℝ) ≤ C * ((n : ℝ) / k + k) * Real.logb 2 k := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P81

end

Source

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

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$ , $n\geq n_0$ , and $2\log^*n\leq k$ , and every $v_1\in\{0,\ldots,n-1\}$ , there exist a natural number $c$ and a public-randomness classical protocol $P$ on inputs $a,b:\{0,\ldots,n-1\}\to\{0,\ldots,n-1\}$ with the following properties. Here

\Lambda_0(x)=\max(1,x),\qquad \Lambda_{j+1}(x)=\max(1,\log_2\Lambda_j(x)),\qquad \log^*n=\inf\{j\in\mathbb N:\Lambda_j(n)\leq1\},

with the infimum taken in the natural numbers. The protocol is a finite weighted collection of deterministic binary communication trees, with nonnegative weights summing to $1$ ; each transmitted bit depends only on its sender's input, and each leaf outputs a function of one party's input. For every positive-weight seed, each root-to-leaf path transmits at most $c$ bits and has at most $k$ rounds when counted as the number of consecutive same-sender transmission blocks plus one if the first sender is Alice, with zero rounds for a path having no transmissions. For every input pair, the total weight of trees outputting the vertex obtained from $L(v_1)$ after exactly $k+1$ steps of $L(v)\mapsto R(a(v))$ , $R(v)\mapsto L(b(v))$ is at least $2/3$ . Finally,

c\leq C\left(\frac nk+k\right)\log_2 k.

The constants $C,n_0$ are common to all admissible $k,n,v_1$ , and zero-weight seeds need not obey the communication bounds.

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