Three initial rounds yield dyadic QMA error decay
ProvedShiQMAErrorIteration.dyadic_error_boundamplificationqmaquantum-complexity
For the majority-of-three error recurrence starting at , every natural number satisfies . Thus a logarithmic number of further rounds reaches any specified exponential error exponent.
Preamble
import Definitions.Def_ShiQMAErrorIteration import Theorems.Thm_ShiQMAErrorIteration_scaled_error_bound set_option autoImplicit false open ShiQMAErrorIteration
Formal statement
theorem ShiQMAErrorIteration.dyadic_error_bound (r : Nat) :
error (r + 3) ≤ ((1 : ℝ) / 2) ^ (2 ^ r) := by sorrySource
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