In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults, Lambda
from proveit import a, b, m, t
from proveit.logic import And, Iff
from proveit.numbers import zero, two, Less, LessEq, greater, Exp
from proveit.physics.quantum.algebra import Ket
from proveit.physics.quantum.QPE import ModAdd
from proveit.physics.quantum.QPE import (
_phase, _alpha_ideal_case, _outcome_prob, _phase_in_interval,
_t, _t_in_natural_pos, _two_pow_t_is_nat_pos)
In [2]:
%proving qpe_exact
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
qpe_exact:
(see dependencies)
qpe_exact:
(see dependencies)
First, we'll prove the instance expression in terms of the local QPE literals¶
In [3]:
_outcome_prob
In [4]:
_alpha_ideal_case
In [5]:
defaults.assumptions = [_alpha_ideal_case.antecedent]
defaults.assumptions: 
In [6]:
alpha_eq1 = _alpha_ideal_case.derive_consequent()
alpha_eq1: 
⊢ 
⊢ 
In [7]:
_m = alpha_eq1.lhs.index
_m: 
In [8]:
prob_eq_1 = _outcome_prob.instantiate({m:_m}, replacements=[alpha_eq1])
prob_eq_1: ⊢ 
⊢ 
In [9]:
qpe_exact_with_extra_cond = prob_eq_1.generalize(
qpe_exact.instance_param_lists(),
conditions=qpe_exact.all_conditions() + [_phase_in_interval])
qpe_exact_with_extra_cond: ⊢ 
In [ ]:
This has an extra condition that we will eliminate as redundant¶
Specifically, $\varphi \in [0, 1)$ is redundant given $2^t \varphi \in \{0 .. 2^t - 1\}$.
In [10]:
desired_phase_cond = qpe_exact.instance_expr.instance_expr.instance_expr.condition
desired_phase_cond: 
In [11]:
defaults.assumptions = qpe_exact.all_conditions()[:-3] + [desired_phase_cond]
defaults.assumptions: 
In [12]:
phase_cond = qpe_exact.all_conditions()[-2]
phase_cond:
In [13]:
phase_cond_lower_bound = phase_cond.derive_element_lower_bound()
phase_cond_lower_bound: 
, ⊢ 
, ⊢ 
In [14]:
phase_cond_lower_bound.divide_both_sides(Exp(two, t))
, ⊢ 
In [15]:
phase_cond_upper_bound_01 = phase_cond.derive_element_upper_bound()
phase_cond_upper_bound_01: , ⊢ 
, ⊢ 
In [16]:
phase_cond_upper_bound_02 = phase_cond_upper_bound_01.divide_both_sides(
Exp(two, t)).inner_expr().rhs.distribute()
phase_cond_upper_bound_02: , ⊢ 
, ⊢ 
In [17]:
inv_two_pow_t_is_pos = greater(phase_cond_upper_bound_02.rhs.operands[1].operand, zero).prove()
inv_two_pow_t_is_pos: ⊢ 
⊢ 
In [18]:
phase_cond_upper_bound_02.rhs.deduce_bound(inv_two_pow_t_is_pos)
In [19]:
_phase_in_interval.literals_as_variables(_phase, _t).prove()
, ⊢ 
In [ ]:
Now we can replace the $\varphi$ condition with the right one¶
In [20]:
phase_cond = qpe_exact_with_extra_cond.instance_expr.instance_expr.instance_expr.condition.prove()
phase_cond: , ⊢ 
, ⊢ 
In [21]:
qpe_exact_with_extra_cond.instance_expr.instance_expr.instance_expr.operand.body
In [22]:
conditional = qpe_exact_with_extra_cond.instance_expr.instance_expr.instance_expr.operand.body
conditional: 
In [23]:
cond_equiv = Iff(phase_cond.expr, desired_phase_cond).prove(assumptions=qpe_exact.all_conditions()[:-3])
cond_equiv: ⊢ 
⊢ 
In [24]:
defaults.assumptions = []
defaults.assumptions: 
In [25]:
qpe_exact_done = (qpe_exact_with_extra_cond.inner_expr().instance_expr.instance_expr
.instance_expr.operand.body.substitute_condition(cond_equiv, assumptions=[]))
qpe_exact_done: ⊢ 
In [26]:
%qed
Out[26]:
