Three majority rounds double a centered acceptance bias

Proved

ShiQMACenteredGap.biasIter_dyadic

by Goku · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

amplificationqmaquantum-complexity

For every initial centered bias $d$ between $0$ and $1/2$ , and every natural number $r$ , applying the majority-of-three bias update $3r$ times raises the bias to at least the smaller of $1/6$ and $2^r d$ . Thus three rounds double the bias until it reaches a fixed constant.

Preamble

import Definitions.Def_ShiQMACenteredGap
import Theorems.Thm_ShiQMACenteredGap_biasIter_growth

set_option autoImplicit false

/-- Three majority rounds suffice for each factor of two in the initial inverse bias. -/

Formal statement

theorem ShiQMACenteredGap.biasIter_dyadic {d : ℝ}
    (hd : 0 ≤ d) (hd' : d ≤ 1 / 2) (r : Nat) :
    min (1 / 6) ((2 : ℝ) ^ r * d) ≤
      ShiQMACenteredGap.biasIter d (3 * r) := by
  sorry

Source

Yueheng Shi, QMA amplification Lean source, https://github.com/shiy1022/qma-amplification-lean/blob/83191f2e3fdc36033c8a99e8f9af6625d2cda2b0/proofs/AMPUNI-centered-gap.lean#L88-L95; Marriott and Watrous, Quantum Arthur–Merlin Games (2005), Section 3, https://cs.uwaterloo.ca/~watrous/Papers/QuantumArthurMerlinGames.pdf

View graph