Concrete uniform-generator schedule reaches target QMA error
ProvedShiQMACenteredGap.existing_rounds_sufficeamplificationqmaquantum-complexityscheduleuniformity
The existing generator round count reaches the centered bias required for the target exponential error under an inverse-polynomial starting gap.
Preamble
import Definitions.Def_ShiQMACenteredGapDominatingSchedule import Theorems.Thm_ShiQMACenteredGap_generalGapRounds_suffice import Theorems.Thm_ShiQMACenteredGap_biasIter_rounds_mono import Theorems.Thm_ShiQMACenteredGap_generalGapRounds_le_existing set_option autoImplicit false set_option maxHeartbeats 2000000 open ShiQMACenteredGap ShiQMAConstructiveSchedule
Formal statement
theorem ShiQMACenteredGap.existing_rounds_suffice {d : ℝ} (hd₀ : 0 ≤ d) (hd₁ : d ≤ 1 / 2)
(q p : Polynomial ℕ) (n : Nat) (hgap : (1 / 6 : ℝ) ≤ (↑(q.eval n) : ℝ) * d) :
1 / 2 - ((1 : ℝ) / 2) ^ (p.eval n) ≤
biasIter d (rounds (gapPolynomial q p) n) := by sorrySource