Scaled majority-of-three error decays doubly exponentially

Proved

ShiQMAErrorIteration.scaled_error_bound

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

amplificationqmaquantum-complexity

Let $e_0=1/3$ and $e_{k+1}=3e_k^2-2e_k^3$ . For every natural number $r$ , the scaled error after $r+1$ rounds satisfies $3e_{r+1}\le (7/9)^{2^r}$ . This gives a quantitative decay law for repeated majority-of-three amplification.

Preamble

import Definitions.Def_ShiQMAErrorIteration

set_option autoImplicit false
open ShiQMAErrorIteration

Formal statement

theorem ShiQMAErrorIteration.scaled_error_bound (r : Nat) :
    3 * error (r + 1) ≤ ((7 : ℝ) / 9) ^ (2 ^ r) := 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