Theorems (or conjectures) for the theory of proveit.physics.quantum.QPE

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import a, b, e, k, l, m, n, r, s, t, u, U, eps
from proveit import IndexedVar, ExprRange,  Lambda
from proveit.logic import (
    Implies, And, Or, Equals, Forall, Exists, Set, InSet, InClass, NotEquals, NotInSet,
    SubsetEq, Difference, Set, SetOfAll, Disjoint, Bijections)
from proveit.numbers import (
    zero, one, two, three, four, pi, i,
    Abs, Add, Complex, Div, Exp, exp, exp2pi_i, sqrd, frac, greater, greater_eq,
    Integer, IntegerNonZero, IntegerNeg, Interval, IntervalCC, IntervalCO,
    number_ordering,
    IntervalOC, IntervalOO, Less, LessEq, Mod, ModAbs, Round, Mult, Natural,
    NaturalPos, Neg, Real, RealNonNeg, sqrd, sqrt, subtract, Sum)
from proveit.linear_algebra import (
    MatrixMult, Norm, ScalarMult, TensorProd, Unitary, VecAdd, VecSum)
from proveit.statistics import Prob, ProbOfAll, SampleSpaces
from proveit.physics.quantum import Bra, Meas, NumBra, NumKet, Qmult, QubitRegisterSpace
from proveit.physics.quantum import inv_root2, ket0, ket1, normalized_var_ket_u, var_ket_u 
from proveit.physics.quantum.QPE import (
    _alpha, _alpha_l, _alpha_bl, _alpha_l_sqrd, _alpha_m, _alpha_m_sqrd, _rel_indexed_alpha,
    _b, _b_floor, _b_round, _delta, _delta_b, _delta_b_floor, _delta_b_round,
    _diff_l_scaled_delta_floor, _e_domain, _eps, _full_domain,
    _ideal_phase_cond, _ket_u, _m_domain, _n, _n_ge_two,
    _neg_domain, _Omega, phase, _phase, _phase_est, phase_est, _phase_in_interval,
    _phase_circuit, _phase_est_circuit, _phase_est_circuit_b_r, _pos_domain, _Psi_ket, _psi,
    _Psi_register_meas, _psi_t_circuit, _Psi_circuit, _psi_t_ket, _s,
    _s_in_nat_pos, s_ket_domain, _sample_space, _success_cond, _t,
    _t_in_natural_pos, _t_req, two_pow_s, two_pow_t, _two_pow_t, _U, _U_pow_two_pow_k
    )
from proveit.physics.quantum.QPE.phase_est_ops import (
    exp2pi_i_on_two_pow_t, exp_neg_2pi_i_on_two_pow_t, ModAdd, Psuccess, Pfail, SubIndexed )
from proveit.physics.quantum.QFT import InverseFourierTransform
from proveit.trigonometry import Sin
from IPython.display import display

%begin theorems

Defining theorems for theory 'proveit.physics.quantum.QPE'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

The main theorems: QPE circuit output

These main theorems are proven using the "local theorems" below via "literal generalization" in which we convert literals to variables and eliminate extraneous theorem/axiom dependencies. That is, local definitions (e.g., definitions for $t$, $U$, $\oplus$, $P_{\textrm fail}$, etc. in the axioms notebook) are used for convenience to prove local theorems but are formally eliminated to prove these statements that quantify over $t$, $U$, etc. and become logically independent of the local definitions.

qpe_exact = (
    Forall((s, t),
    Forall(U,
    Forall(var_ket_u,
    Forall(phase,
           Equals(Prob(_phase_circuit.literals_as_variables(_s, _t, _U, _ket_u, _phase)), one),
           domain=Real,
           conditions=[_ideal_phase_cond.literals_as_variables(_t, _phase), 
                       Equals(MatrixMult(U, var_ket_u),
                       ScalarMult(exp2pi_i(phase), var_ket_u))]).with_wrapping(),
    domain=s_ket_domain, condition=normalized_var_ket_u).with_wrapping(),
    domain=Unitary(two_pow_s)).with_wrapping(),
    domain=NaturalPos).with_wrapping())

qpe_exact (conjecture with conjecture-based proof):

from proveit.physics.quantum.QPE import _phase_est_circuit_b_r
qpe_best_guarantee = (
    Forall((s, t), Forall(U, Forall(var_ket_u, Forall(phase,
        greater(Prob(_phase_est_circuit_b_r.literals_as_variables(_s, _t, _U, _ket_u, _phase)),
                frac(four, Exp(pi, two))),
        domain=Real,
        conditions=[_phase_in_interval.literals_as_variables(_phase),
                    Equals(MatrixMult(U, var_ket_u),
                    ScalarMult(exp2pi_i(phase), var_ket_u))]).with_wrapping(),
    domain=s_ket_domain, condition=normalized_var_ket_u).with_wrapping(),
    domain=Unitary(two_pow_s)).with_wrapping(),
    domain=NaturalPos).with_wrapping())

qpe_best_guarantee (conjecture with conjecture-based proof):

qpe_precision_guarantee = Forall(
    eps, Forall(
        (s, n), Forall(
            (U, var_ket_u, phase), 
            Forall(
                t, greater_eq(
                    ProbOfAll(m, _phase_est_circuit.literals_as_variables(_s, _t, _U, _ket_u, _phase),
                              domain=_m_domain.literals_as_variables(_t), 
                              condition=_success_cond.literals_as_variables(_t, _n, _phase))
                    .with_wrapping(), 
                    subtract(one, _eps.as_variable())),
                domain=NaturalPos,
                condition=_t_req.literals_as_variables(_t, _n, _eps)).with_wrapping(),
            domains=(Unitary(two_pow_s), s_ket_domain, Real),
            conditions=[_phase_in_interval.literals_as_variables(_phase),
                        normalized_var_ket_u,
                        Equals(MatrixMult(U, var_ket_u),
                               ScalarMult(exp2pi_i(phase), var_ket_u))]).with_wrapping(),
        domain=NaturalPos, condition=_n_ge_two.literals_as_variables(_n)).with_wrapping(),
    domain=IntervalOC(zero, one)).with_wrapping()

qpe_precision_guarantee (conjecture with conjecture-based proof):

main_theorems_combined = And(qpe_exact, qpe_best_guarantee, qpe_precision_guarantee).with_wrapping_at(1, 3)

main_theorems_combined (conjecture with conjecture-based proof):

Local theorems (for convenience - used only internally)

Match quantum circuit outputs with definitions for $|\psi_t \rangle$ and $|\Psi\rangle$.

For the _psi_t_output theorem below, the initial-stage circuit output $\lvert \psi_{t} \rangle$ is defined in the QPE axioms as

$\lvert \psi_{t} \rangle = (\frac{1}{\sqrt{2}}(\lvert 0 \rangle + e^{2\pi i 2^{t-1}}\lvert 1 \rangle)) \otimes (\frac{1}{\sqrt{2}}(\lvert 0 \rangle + e^{2\pi i 2^{t-2}}\lvert 1 \rangle)) \otimes \cdots \otimes (\frac{1}{\sqrt{2}}(\lvert 0 \rangle + e^{2\pi i 2^{0}}\lvert 1 \rangle))$

_psi_t_output = Forall(t, Equals(Prob(_psi_t_circuit.literals_as_variables(_t)), one), 
                       domain=NaturalPos)

_psi_t_output (conjecture with conjecture-based proof):

For the _Psi_output theorem below, the circuit output $\lvert \Psi \rangle$ is defined in the QPE axioms as the result of the inverse quantum Fourier transform applied to the initial-stage output $\lvert \psi \rangle$:

$\lvert \Psi \rangle = \text{FT}^{\dagger} \lvert \psi \rangle$

_Psi_output = Equals(Prob(_Psi_circuit), one)

_Psi_output (conjecture with conjecture-based proof):

Establish the probabilistic sample space $\Omega$ of measurement outcomes.

_sample_space_bijection = (
    InSet(Lambda(_sample_space.instance_param, _sample_space.instance_expr), 
          Bijections(_sample_space.domain, _Omega)))

_sample_space_bijection (conjecture with conjecture-based proof):

_outcome_prob = Forall(
    m, Equals(Prob(_phase_est_circuit), sqrd(Abs(SubIndexed(_alpha, m)))),
    domain=_m_domain)

_outcome_prob (conjecture with conjecture-based proof):

_Omega_is_sample_space = InClass(_Omega, SampleSpaces)

_Omega_is_sample_space (conjecture with conjecture-based proof):

Simplify $|\psi_t \rangle$ and evaluate $\alpha_l \equiv \lvert b \oplus l \rangle$ as the amplitudes of $\lvert \Psi \rangle$ relative to the $t$-bit estimate of $2^t \varphi$, $b$.

This _psi_t_formula theorem corresponds to Nielsen & Chuang's (2010) formula 5.20 (pg 222).

# Notice we're using a ScalarMults instead of QMults on the rhs
# at least until QMults are automatically simplified to do that instead
_psi_t_formula = Forall(
    t, Equals(_psi_t_ket,
              ScalarMult(frac(one, Exp(two, frac(t, two))),
                    VecSum(k, ScalarMult(exp(Mult(two, pi, i, _phase, k)), NumKet(k, t)),
                           domain=Interval(zero, subtract(Exp(two, t), one))))),
    domain=NaturalPos)

_psi_t_formula (conjecture with conjecture-based proof):

The following _alpha_m_evaluation theorem gives an evaluation formula for the amplitude of the possible measurement outcome $\lvert m \rangle$. This is a step between Nielsen & Chuang's formulas 5.23 and 5.24 (pg 223), from which we are then able to derive a formula analogous to their formula 5.24. We don't explicitly derive a separate theorem analogous to Nielsen & Chuang's formula 5.23; instead we prove the _alpha_m_evaluation theorem via the application of the inverse quantum Fourier transform to the result in the _psi_t_formula theorem.

_alpha_m_evaluation = Forall(
        m,
        Equals(_alpha_m,
               Mult(frac(one, _two_pow_t),
                   Sum(k, Mult(exp_neg_2pi_i_on_two_pow_t(k, m),
                               exp2pi_i(_phase, k)),
                       domain=Interval(zero, subtract(_two_pow_t, one))))),
        domain=_m_domain)

_alpha_m_evaluation (conjecture with conjecture-based proof):

The _alpha_ideal_case theorem:
When the scaled phase $2^{t} \varphi$ can be represented in $t$ (or fewer) bits (what Nielsen & Chuang called "the ideal case"),
the probability amplitude $\alpha_{m}$ of measurement $m = 2^{t}\varphi$ is $1$.

_alpha_ideal_case = (
    Implies(_ideal_phase_cond, Equals(SubIndexed(_alpha, Mult(_two_pow_t, _phase)), one)))

_alpha_ideal_case (conjecture with conjecture-based proof):

from proveit.physics.quantum.QPE import _alpha_m_mod_two_pow_t
_alpha_m_mod_evaluation = (
    Forall(
        m,
        Equals(_alpha_m_mod_two_pow_t,
               Mult(frac(one, _two_pow_t),
                   Sum(k, Mult(exp_neg_2pi_i_on_two_pow_t(k, m),
                               exp2pi_i(_phase, k)),
                       domain=Interval(zero, subtract(_two_pow_t, one))))),
        domain=Integer))

_alpha_m_mod_evaluation (conjecture with conjecture-based proof):

from proveit.physics.quantum.QPE import _alpha_m_mod_two_pow_t
_alpha_m_mod_as_geometric_sum = (
    Forall(
        m,
        Equals(_alpha_m_mod_two_pow_t,
               Mult(frac(one, _two_pow_t),
                   Sum(k, Exp(exp2pi_i(subtract(_phase, frac(m, _two_pow_t))), k),
                       domain=Interval(zero, subtract(_two_pow_t, one))))),
        domain=Integer))

_alpha_m_mod_as_geometric_sum (conjecture with conjecture-based proof):

# Lower bound on the probability of obtaining the rounding-based best estimate b_r,
# assuming delta ≠ 0 (i.e. assuming the non-exact case)
_best_guarantee_delta_nonzero = (
        Implies(NotEquals(_delta_b_round, zero),
                greater(sqrd(Abs(SubIndexed(_alpha, Mod(_b_round, _two_pow_t)))),
                           frac(four, Exp(pi, two)))))

_best_guarantee_delta_nonzero (conjecture with conjecture-based proof):

_best_guarantee = (
        greater(sqrd(Abs(SubIndexed(_alpha, Mod(Round(Mult(_two_pow_t, _phase)), _two_pow_t)))),
                frac(four, Exp(pi, two))))

_best_guarantee (conjecture with conjecture-based proof):

Evaluation of $\alpha_l$ after performing the geometric series summation in terms of $\delta$:

The _alpha_summed theorem corresponds to Nielsen & Chuang's formula 5.26 (pg 224).

_alpha_summed = Forall(
    l,
    Equals(SubIndexed(_alpha, ModAdd(_b_floor, l)),
           Mult(frac(one, _two_pow_t),
                    frac(subtract(one, exp2pi_i(subtract(Mult(_two_pow_t, _delta_b_floor), l))),
                         subtract(one, exp2pi_i(subtract(_delta_b_floor, frac(l, _two_pow_t))))))),
    domain=_full_domain,
    condition=NotEquals(l, zero))

_alpha_summed (conjecture with conjecture-based proof):

Compute the probability of failure with a measurement beyond $e$ units away from $b$.

The _fail_sum theorem corresponds to Nielsen & Chuang's formula 5.27 (pg 224). We also abstract out a section of its proof into a smaller lemma to prove the logical equivalence of two similar conditions.

from proveit.logic import Iff, Union
_fail_sum_prob_conds_equiv_lemma = (
    Forall(l,
        Forall(
            e,
            Iff(And(InSet(l, Union(_neg_domain, _pos_domain)), greater(ModAbs(l, _two_pow_t), e)),
                And(InSet(l, _full_domain), greater(ModAbs(l, _two_pow_t), e)) ).with_wrap_before_operator(),
            domain=_e_domain).with_wrapping()).with_wrapping())

_fail_sum_prob_conds_equiv_lemma (conjecture with conjecture-based proof):

_fail_sum = (
    Forall(
        e,
        Equals(Pfail(e),
               Add(Sum(l, Exp(Abs(_rel_indexed_alpha), two), domain=_neg_domain),
                   Sum(l, Exp(Abs(_rel_indexed_alpha), two), domain=_pos_domain))),
        domain=_e_domain))

_fail_sum (conjecture with conjecture-based proof):

The _alpha_sqrd_upper_bound theorem is derived from _alpha_summed, and Nielsen & Chuang's formula 5.29 (pg 224) appears as a step in the interactive proof notebook steps:

from proveit.physics.quantum.QPE import _delta_b_floor
_alpha_sqrd_upper_bound = Forall(
    l,
    LessEq(Exp(Abs(SubIndexed(_alpha, ModAdd(_b_floor, l))), two),
           frac(one,
                Mult(four, Exp(subtract(l, Mult(_two_pow_t, _delta_b_floor)), two)))),
    domain=_full_domain,
    condition=NotEquals(l, zero))

_alpha_sqrd_upper_bound (conjecture with conjecture-based proof):

Obtain a bound on the failure probability:

The _failure_upper_bound_lemma theorem corresponds to Nielsen & Chuang's formula 5.30 (pg 224), establishing an initial expression for the probability of failing to obtain a sufficiently accurate estimate:

_failure_upper_bound_lemma = Forall(
    e,
    LessEq(Pfail(e), 
           Mult(frac(one, four), 
                Add(Sum(l, frac(one, sqrd(_diff_l_scaled_delta_floor)), domain=_neg_domain),
                    Sum(l, frac(one, sqrd(_diff_l_scaled_delta_floor)), domain=_pos_domain)))), 
    domain=_e_domain)

_failure_upper_bound_lemma (conjecture with conjecture-based proof):

And then _failure_upper_bound corresponds to Nielsen & Chuang's formula 5.34 (pg 224), but derived in a slightly different way to allow two distinctions from Nielsen & Chuang's result: (1) the bound now works for $e = 1$; (2) the bound is now somewhat tighter.

_failure_upper_bound = Forall(
    e,
    LessEq(Pfail(e), Add(frac(one, Mult(two, e)), frac(one, Mult(four, Exp(e, two))) )),
    domain=_e_domain)

_failure_upper_bound (conjecture with conjecture-based proof):

Evaluate the success probability as the complement of failure and establish our precision guarantee.

_success_complements_failure  = Forall(
        e, Equals(Psuccess(e), subtract(one, Pfail(e))),
        domain=_e_domain)

_success_complements_failure (conjecture with conjecture-based proof):

Taking Nielsen & Chuang's formula 5.35 (pg 224) as an axiom for the number of qubits in the top register, $t = \left(n + \left\lceil \textrm{log}_2\left(2 + \frac{1}{2 \cdot \epsilon}\right)\right\rceil\right)$, we derive a precision guarantee probability greater than $1 - \epsilon$. That is, rather then deriving the number of qubits needed for a certain precision and success probability as done by Nielsen & Chuang, we derive that a given number of qubits is sufficient.

The _precision_guarantee_lemma_01 and …_lemma_02 theorems below are both used in the proof the the _precision_guarantee theorem.

_precision_guarantee_lemma_01 = (
    greater(Add(one,
         Neg(frac(one, Mult(two, subtract(Exp(two, subtract(_t, _n)), one)))),
         Neg(frac(one, Mult(four, Exp(subtract(Exp(two, subtract(_t, _n)), one), two))))),
     subtract(one, _eps)))

_precision_guarantee_lemma_01 (conjecture with conjecture-based proof):

_precision_guarantee_lemma_02 = (
        Forall(m,
           _success_cond,
           domain = _m_domain,
           condition = LessEq(ModAbs(subtract(m, _b_floor), _two_pow_t),
                              subtract(Exp(two, subtract(_t, _n)), one)))
        )

_precision_guarantee_lemma_02 (conjecture with conjecture-based proof):

_precision_guarantee = greater_eq(
    ProbOfAll(m, _phase_est_circuit,
              domain=_m_domain, condition=_success_cond).with_wrapping(), 
    subtract(one, _eps))

_precision_guarantee (conjecture with conjecture-based proof):

Minor theorems used through-out

# t (represented by the Literal _t) denotes
# the number of Qbits in the input register
# Thus, 2^t is a positive natural number
_two_pow_t_is_nat_pos = InSet(_two_pow_t, NaturalPos)

_two_pow_t_is_nat_pos (conjecture with conjecture-based proof):

# t (represented by the Literal _t) denotes
# the number of Qbits in the input register
_two_pow_t_minus_one_is_nat_pos = InSet(Exp(two, subtract(_t, one)), NaturalPos)

_two_pow_t_minus_one_is_nat_pos (conjecture with conjecture-based proof):

_psi_t_ket_is_normalized_vec = Forall(
    t, And(InSet(_psi_t_ket, QubitRegisterSpace(t)),
           Equals(Norm(_psi_t_ket), one)),
    domain=NaturalPos)

_psi_t_ket_is_normalized_vec (conjecture with conjecture-based proof):

_Psi_ket_is_normalized_vec = And(InSet(_Psi_ket, QubitRegisterSpace(_t)),
                                  Equals(Norm(_Psi_ket), one))

_Psi_ket_is_normalized_vec (conjecture with conjecture-based proof):

_best_floor_is_int = InSet(_b_floor, Integer)

_best_floor_is_int (conjecture with conjecture-based proof):

_best_floor_is_in_m_domain = InSet(_b_floor, _m_domain)

_best_floor_is_in_m_domain (conjecture with conjecture-based proof):

_best_round_is_int = InSet(_b_round, Integer)

_best_round_is_int (conjecture with conjecture-based proof):

# t (represented by the Literal _t) denotes the number of Qbits in the first register
# n (represented by the Literal _n) denotes the desired number of bits of precision
# In Nielsen & Chuang, e = 2^{t-n} - 1 is the max desired error
_e_value_ge_two = greater_eq(subtract(Exp(two, subtract(_t, _n)), one), two)

_e_value_ge_two (conjecture with conjecture-based proof):

_e_value_in_e_domain = InSet(subtract(Exp(two, subtract(_t, _n)), one), _e_domain)

_e_value_in_e_domain (conjecture with conjecture-based proof):

# The o-plus addition denotes addition modulo 2^t, resulting in an integer
_mod_add_closure = Forall((a, b), InSet(ModAdd(a, b), 
                                        Interval(zero, subtract(Exp(two, _t), one))), 
                         domain=Integer)

_mod_add_closure (conjecture with conjecture-based proof):

# The phase phi is in the real interval [0, 1)
_phase_is_real = InSet(_phase, Real)

_phase_is_real (conjecture with conjecture-based proof):

_delta_b_is_real = Forall(b, InSet(_delta_b, Real), domain=Integer)

_delta_b_is_real (conjecture with conjecture-based proof):

This derives from $\delta$ being the difference between $\delta$ and its best $t$-bit estimate (without going over):

_scaled_delta_b_floor_in_interval = InSet(Mult(_two_pow_t, _delta_b_floor), IntervalCO(zero, one))

_scaled_delta_b_floor_in_interval (conjecture with conjecture-based proof):

_scaled_delta_b_round_in_interval = (
    InSet(Mult(_two_pow_t, _delta_b_round), IntervalCO(Neg(frac(one, two)), frac(one, two))))

_scaled_delta_b_round_in_interval (conjecture with conjecture-based proof):

# This provides a more general interval for _delta_b
# to cover both cases: _delta_b_floor & _delta_b_round
_delta_b_in_interval = (
    Forall(
    b,
    InSet(_delta_b, IntervalOC(Neg(frac(one, two)), frac(one, two))),
    domain=Set(_b_floor, _b_round)))

_delta_b_in_interval (conjecture with conjecture-based proof):

_alpha_are_complex = Forall(m, InSet(_alpha_m, Complex), domain=_m_domain)

_alpha_are_complex (conjecture with conjecture-based proof):

_delta_b_is_zero_or_non_int = (
        Forall(
            b,
            Or( Equals(_delta_b, zero),
                NotInSet(_delta_b, Integer)),
            domain=Set(_b_floor, _b_round)
            ))

_delta_b_is_zero_or_non_int (conjecture with conjecture-based proof):

_scaled_delta_b_is_zero_or_non_int = (
        Forall(
            b,
            Or( Equals(Mult(_two_pow_t, _delta_b), zero),
                NotInSet(Mult(_two_pow_t, _delta_b), Integer)),
            domain=Set(_b_floor, _b_round)
            ))

_scaled_delta_b_is_zero_or_non_int (conjecture with conjecture-based proof):

Follows from scaled_delta_in_interval:

_scaled_delta_b_not_eq_nonzeroInt = Forall(
        (b, l), NotEquals(Mult(_two_pow_t, _delta_b), l),
        domains=[Set(_b_floor, _b_round), Integer], conditions = [NotEquals(l, zero)])

_scaled_delta_b_not_eq_nonzeroInt (conjecture with conjecture-based proof):

_delta_b_not_eq_scaledNonzeroInt = Forall(
        (b, l), NotEquals(_delta_b, frac(l, _two_pow_t)),
        domains=[Set(_b_floor, _b_round), Integer],
        conditions = [NotEquals(l, zero)])

_delta_b_not_eq_scaledNonzeroInt (conjecture with conjecture-based proof):

from proveit.physics.quantum.QPE import _delta_b_floor
_delta_b_floor_diff_in_interval = Forall(
        l,
        InSet(subtract(_delta_b_floor, frac(l, _two_pow_t)),
              IntervalCO(Neg(frac(one, two)), frac(one, two))),
        domain=_full_domain)

_delta_b_floor_diff_in_interval (conjecture with conjecture-based proof):

_non_int_delta_b_diff = Forall(
        (b, l),
        NotInSet(subtract(_delta_b, frac(l, _two_pow_t)),
                Integer), 
        domains=[Set(_b_floor, _b_round), _full_domain],
        conditions = [NotEquals(l, zero)])

_non_int_delta_b_diff (conjecture with conjecture-based proof):

_scaled_abs_delta_b_floor_diff_interval = Forall(
        l,
        InSet(Mult(pi, Abs(subtract(_delta_b_floor, frac(l, _two_pow_t)))),
              IntervalOC(zero, Div(pi, two))),
        domain=_full_domain,
        conditions = [NotEquals(l, zero)])

_scaled_abs_delta_b_floor_diff_interval (conjecture with conjecture-based proof):

_pfail_in_real = Forall(e, InSet(Pfail(e), Real), domain=_e_domain)

_pfail_in_real (conjecture with conjecture-based proof):

Modulo addition may be converted to regular addition within $2 \pi i$ exponentiation:

_phase_from_best_with_delta_b = Forall(
    b,
    Equals(_phase, Add(frac(b, _two_pow_t), _delta_b)),
    domain=Integer)

_phase_from_best_with_delta_b (conjecture with conjecture-based proof):

_modabs_in_full_domain_simp = Forall(l, Equals(ModAbs(l, _two_pow_t), Abs(l)),
                                     domain=_full_domain)

_modabs_in_full_domain_simp (conjecture with conjecture-based proof):

%end theorems

Unable to remove /home/wwitzel/Prove-It/packages/proveit/physics/quantum/QPE/__pv_it/theorems/name_to_hash.txt~.
  Skipping clean step (don't worry, it's not critical)
These theorems may now be imported from the theory package: proveit.physics.quantum.QPE