Coin code realizes the intended dyadic probability
ProvedShiQMACenteredGap.encodeCoin_probabilityamplificationbinary-encodingcenteringqmaquantum-complexity
For every j at most 2^k, the executable coin code has probability j/2^k, including the endpoint j=2^k represented by a constant-one code.
Preamble
import Definitions.Def_ShiQMACenteredGapComputableCoin import Theorems.Thm_ShiQMACenteredGap_fractionBits_numerator set_option autoImplicit false
Formal statement
theorem ShiQMACenteredGap.encodeCoin_probability (k j : Nat) (hj : j ≤ 2 ^ k) :
(encodeCoin k j).probability = (j : ℝ) / (2 : ℝ) ^ k := by
sorrySource