Centered majority iterations compose over added round counts
ProvedShiQMACenteredGap.biasIter_addamplificationbiasqmaquantum-complexityschedule
Running r+s majority rounds equals running r rounds and then s more rounds.
Preamble
import Definitions.Def_ShiQMACenteredGapGeneralSchedule set_option autoImplicit false set_option maxHeartbeats 2000000 open ShiQMACenteredGap ShiQMAErrorIteration ShiQMAConstructiveSchedule
Formal statement
theorem ShiQMACenteredGap.biasIter_add (d : ℝ) (r s : Nat) :
biasIter d (r + s) = biasIter (biasIter d r) s := by sorrySource