The logarithmic majority schedule uses quadratically many copies

Proved

ShiQMAErrorIteration.copies_roundsFor_le

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

amplificationqmaquantum-complexity

For every positive natural number $m$ , the number of verifier copies in the logarithmic majority-of-three schedule is at most $81m^2$ : $3^{R(m)}\le81m^2$ . This supplies a concrete polynomial witness and circuit resource bound.

Preamble

import Definitions.Def_ShiQMAErrorIteration

set_option autoImplicit false
open ShiQMAErrorIteration

Formal statement

theorem ShiQMAErrorIteration.copies_roundsFor_le (m : Nat) (hm : 0 < m) : 3 ^ roundsFor m ≤ 81 * m ^ 2 := 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