Constructive QMA repetition uses polynomially many copies
ProvedShiQMAConstructiveSchedule.copies_rounds_leamplificationpolynomial-boundsqmaquantum-complexity
Three to the constructive round count is bounded by an explicit constant depending on the target polynomial times a fixed power of n+1.
Preamble
import Definitions.Def_ShiQMAConstructiveSchedule set_option autoImplicit false set_option maxHeartbeats 2000000 open ShiQMAConstructiveSchedule ShiQMAErrorIteration
Formal statement
theorem ShiQMAConstructiveSchedule.copies_rounds_le (p : Polynomial ℕ) (n : ℕ) :
3 ^ rounds p n ≤
3 ^ (Nat.log 2 (p.eval 1 + 1) + p.natDegree + 4) *
(n + 1) ^ (2 * p.natDegree) := by sorrySource