Quadratic copy bound including zero target exponent
ProvedShiQMAVariableRounds.copies_roundsFor_le_allamplificationqmaquantum-complexityresourcesuniformity
The number of witness copies at the logarithmic round count is quadratically bounded for every target exponent, including zero.
Preamble
import Definitions.Def_ShiQMAVariableRoundsPolynomialFamily import Theorems.Thm_ShiQMAErrorIteration_copies_roundsFor_le set_option autoImplicit false set_option maxHeartbeats 2000000 open ShiShallow ShiClassQMA ShiQMAErrorIteration Polynomial ShiQMAVariableRounds
Formal statement
theorem ShiQMAVariableRounds.copies_roundsFor_le_all (m : Nat) :
3 ^ roundsFor m ≤ 81 * (m + 1) ^ 2 := by sorrySource