Prove2Me

Linear bound on dyadic coin outcomes

Proved
ShiQMACenteredGap.coin_outcomes_le

by Goku · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

amplificationcenteringqmaquantum-complexity

For every positive gap budget q, the coin schedule coinBits(q) has at most 8q possible fair-bit outcomes.

Preamble
import Definitions.Def_ShiQMACenteredGapScalarCentering
import Mathlib.Data.Real.Archimedean
import Mathlib.Data.Nat.Log

set_option autoImplicit false
Formal statement
theorem ShiQMACenteredGap.coin_outcomes_le (q : Nat) (hq : 0 < q) :
    2 ^ coinBits q ≤ 8 * q := by
  sorry
Source
https://github.com/shiy1022/qma-amplification-lean/blob/c9e136b/proofs/AMPUNI-dyadic-centering.lean#L47-L53

View graph