Positive QMA gap excludes the constant-one centering coin
ProvedShiQMAGeneralGap.thresholdCoinNumerator_ltamplificationbinary-encodingqmaquantum-complexitythresholds
For nonnegative soundness and positive inverse-polynomial threshold gap, the computed centering numerator is strictly below its dyadic denominator.
Preamble
import Definitions.Def_ShiQMAGeneralGapThresholdCoin import Theorems.Thm_ShiQMAGeneralGap_thresholdCoinNumerator_spec set_option autoImplicit false set_option maxHeartbeats 2000000 open ShiQMAGeneralGap ShiQMACenteredGap ShiQMAConstructiveSchedule
Formal statement
theorem ShiQMAGeneralGap.thresholdCoinNumerator_lt {a b : Nat → ℝ}
(A : ThresholdApproximation a) (B : ThresholdApproximation b)
(q : Polynomial ℕ) (n : Nat) (hb : 0 ≤ b n) (hab : b n ≤ a n)
(hgap : (1 : ℝ) ≤ (↑(q.eval n) : ℝ) * (a n - b n)) :
thresholdCoinNumerator A B q n < 2 ^ (rounds q n + 1) := by sorrySource