Centered-gap normalization uses polynomially many copies
ProvedShiQMACenteredGap.copies_gapRounds_leamplificationqmaquantum-complexity
For every positive natural , the number of witness copies needed by the centered-gap normalization schedule is bounded by . This gives an explicit polynomial resource bound.
Preamble
import Definitions.Def_ShiQMACenteredGap set_option autoImplicit false open ShiQMAErrorIteration ShiQMACenteredGap
Formal statement
theorem ShiQMACenteredGap.copies_gapRounds_le (q : Nat) (hq : 0 < q) :
3 ^ gapRounds q ≤ 27 * q ^ 5 := by sorrySource
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