Majority amplification preserves centered bias order
ProvedShiQMACenteredGap.biasStep_monoamplificationbiasqmaquantum-complexityschedule
The centered majority update is monotone on biases between zero and one half.
Preamble
import Definitions.Def_ShiQMACenteredGapGeneralSchedule set_option autoImplicit false set_option maxHeartbeats 2000000 open ShiQMACenteredGap ShiQMAErrorIteration ShiQMAConstructiveSchedule
Formal statement
theorem ShiQMACenteredGap.biasStep_mono {d e : ℝ} (hd : 0 ≤ d) (hde : d ≤ e)
(he : e ≤ 1 / 2) : biasStep d ≤ biasStep e := by sorrySource