A centered majority round never decreases valid bias
ProvedShiQMACenteredGap.biasStep_geamplificationqmaquantum-complexityscheduleuniformity
On the nonnegative half interval, one majority update is at least the original bias.
Preamble
import Definitions.Def_ShiQMACenteredGapDominatingSchedule set_option autoImplicit false set_option maxHeartbeats 2000000 open ShiQMACenteredGap ShiQMAConstructiveSchedule
Formal statement
theorem ShiQMACenteredGap.biasStep_ge {d : ℝ} (hd₀ : 0 ≤ d) (hd₁ : d ≤ 1 / 2) : d ≤ biasStep d := by sorrySource