Fixed-width binary encoder recovers its numerator
ProvedShiQMACenteredGap.fractionBits_numeratoramplificationbinary-encodingcenteringqmaquantum-complexity
For every j smaller than 2^k, decoding the k-bit fractional encoding of j returns exactly j.
Preamble
import Definitions.Def_ShiQMACenteredGapComputableCoin set_option autoImplicit false
Formal statement
theorem ShiQMACenteredGap.fractionBits_numerator (k j : Nat) (hj : j < 2 ^ k) :
binaryNumerator (fractionBits k j) = j := by
sorrySource