Centered majority bias equals half minus majority error
ProvedShiQMACenteredGap.biasIter_standardamplificationqmaquantum-complexity
Starting at centered bias , after any majority-of-three rounds the bias is exactly minus the standard majority-error recurrence after rounds. This identifies the centered and error viewpoints used in the QMA amplification schedule.
Preamble
import Definitions.Def_ShiQMACenteredGap set_option autoImplicit false /-- Centered majority bias is the complement of the standard error recurrence. -/
Formal statement
theorem ShiQMACenteredGap.biasIter_standard (r : Nat) :
ShiQMACenteredGap.biasIter (1 / 6) r =
1 / 2 - ShiQMAErrorIteration.error r := by
sorrySource
Yueheng Shi, QMA amplification Lean source, https://github.com/shiy1022/qma-amplification-lean/blob/83191f2e3fdc36033c8a99e8f9af6625d2cda2b0/proofs/AMPUNI-general-gap-schedule.lean#L23-L29; Marriott and Watrous, Quantum Arthur–Merlin Games (2005), Section 3, https://cs.uwaterloo.ca/~watrous/Papers/QuantumArthurMerlinGames.pdf