A logarithmic schedule turns an inverse-polynomial bias into a constant

Proved

ShiQMACenteredGap.biasIter_gapRounds

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

amplificationqmaquantum-complexity

Suppose $0\le d\le1/2$ and $qd\ge1/6$ for a natural number $q$ . After $3(\lfloor\log_2q\rfloor+1)$ majority-of-three rounds, the iterated centered bias is at least $1/6$ .

Preamble

import Definitions.Def_ShiQMACenteredGap
import Theorems.Thm_ShiQMACenteredGap_biasIter_growth

set_option autoImplicit false
open ShiQMAErrorIteration ShiQMACenteredGap

Formal statement

theorem ShiQMACenteredGap.biasIter_gapRounds {d : ℝ} (hd : 0 ≤ d) (hd' : d ≤ 1 / 2)
    (q : Nat) (hgap : (1 / 6 : ℝ) ≤ (q : ℝ) * d) :
    (1 / 6 : ℝ) ≤ biasIter d (gapRounds q) := by sorry

Source

Yueheng Shi, AMPUNI-centered-gap.lean, formal bias analysis for copy-based QMA amplification; context: Marriott and Watrous, Quantum Arthur–Merlin Games (2005), Section 3, Theorem 3, https://cs.uwaterloo.ca/~watrous/Papers/QuantumArthurMerlinGames.pdf

View graph