A logarithmic majority schedule meets any dyadic error target

Proved

ShiQMAErrorIteration.error_roundsFor

by Goku · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

amplificationqmaquantum-complexity

Define the number of majority-of-three rounds by $R(m)=\lfloor\log_2m\rfloor+4$ . For every natural target exponent $m$ , the resulting error is at most $2^{-m}$ , including the small cases $m=0$ and $m=1$ .

Preamble

import Definitions.Def_ShiQMAErrorIteration
import Theorems.Thm_ShiQMAErrorIteration_dyadic_error_bound

set_option autoImplicit false
open ShiQMAErrorIteration

Formal statement

theorem ShiQMAErrorIteration.error_roundsFor (m : Nat) : error (roundsFor m) ≤ ((1 : ℝ) / 2) ^ m := by sorry

Source

Marriott and Watrous, Quantum Arthur–Merlin Games (2005), Section 3, Theorem 3, https://cs.uwaterloo.ca/~watrous/Papers/QuantumArthurMerlinGames.pdf; original Lean proof: Yueheng Shi, AMPUNI-error-iteration.lean

View graph