General-gap round count has affine-logarithmic controller form
ProvedShiQMACenteredGap.generalGapRounds_controller_formamplificationbiasqmaquantum-complexityschedule
The sum of normalization and error-reduction rounds equals an explicit affine expression in the logarithm of input length plus one.
Preamble
import Definitions.Def_ShiQMACenteredGapGeneralSchedule set_option autoImplicit false set_option maxHeartbeats 2000000 open ShiQMACenteredGap ShiQMAErrorIteration ShiQMAConstructiveSchedule
Formal statement
theorem ShiQMACenteredGap.generalGapRounds_controller_form (q p : Polynomial ℕ) (n : Nat) :
generalGapRounds q p n =
(3 * (Nat.log 2 (q.eval 1 + 1) + 4) + Nat.log 2 (p.eval 1 + 1) + 4) +
(3 * q.natDegree + p.natDegree) * (Nat.log 2 (n + 1) + 1) := by sorrySource