as follows: we require that for some constant c depending on the circuit family. Note this choice does not affect the basic properties of , and also it can be shown that any computation consisting of typical gates (e.g. Hadamard, Toffoli) has this property whenever . Proving ⊆ Suppose we are given a family of circuits to decide a language L. We assume without loss of generality (e.g. see the inessential properties of quantum computers) that all gates have transition matrices that are represented with real numbers, at the expense of adding one more qubit. Let denote the final quantum state of the circuit before the postselecting measurement is made. The overall goal of the proof is to construct a algorithm to decide L. More specifically it suffices to have L correctly compare the squared amplitude of in the states with to the squared amplitude of in the states with to determine which is bigger. The key insight is that the comparison of these amplitudes can be transformed into comparing the acceptance probability of a machine with 1/2. Matrix view of PostBQP algorithms Let n denote the input size, denote the total number of qubits in the circuit (inputs, ancillary, output and postselection qubits), and denote the total number of gates. Represent the ith gate by its transition matrix Ai (a real unitary matrix) and let the initial state be (padded with zeroes). Then . Define S1 (resp. S0) to be the set of basis states corresponding to (resp. ) and define the probabilities The definition of ensures that either or according to whether x is in L or not. Our machine will compare and . In order to do this, we expand the definition of matrix multiplication: where the sum is taken over all lists of G basis vectors . Now and can be expressed as a sum of pairwise products of these terms. Intuitively, we want to design a machine whose acceptance probability is something like , since then would imply that the acceptance probability is , while would imply that the acceptance probability is . Technicality: we may assume entries of the transition matrices are rationals with denominator for some polynomial f(n). The definition of tells us that if x is in L, and that otherwise . Let us replace all entries of A by the nearest fraction with denominator for a large polynomial that we presently