logo

Proof of proveit.physics.quantum.QPE._psi_t_formula theorem

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, c, k, m, n, t, P, defaults, Function
from proveit.linear_algebra import ScalarMult, TensorProd, VecSpaces
from proveit.logic import Equals, InSet
from proveit.numbers import (
        zero, one, two, i, e, pi, Add, Sum, Exp, Less, LessEq, Mult, frac, Neg, subtract)
from proveit.numbers import Complex, Interval, Natural
from proveit.numbers.number_sets.natural_numbers import fold_forall_natural_pos
from proveit.physics.quantum import Ket, NumKet
from proveit.physics.quantum.QPE import _phase, _phase_is_real, _psi_t_def
In [2]:
%proving _psi_t_formula
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_psi_t_formula:
(see dependencies)

Keep the $2$ in $2 \pi i$ from combining with powers of $2$:

In [3]:
Exp.change_simplification_directives(factor_numeric_rational=True)
In [4]:
# the induction theorem for positive naturals
fold_forall_natural_pos
 ⊢  
In [5]:
# instantiate the induction theorem
induction_inst = fold_forall_natural_pos.instantiate(
    {Function(P,t):_psi_t_formula.instance_expr, m:t, n:t})
induction_inst:  ⊢  

Base Case

In [6]:
VecSpaces.default_field=Complex
defaults.assumptions = _psi_t_formula.all_conditions()
defaults.assumptions:
In [7]:
base_case = induction_inst.antecedent.operands[0]
base_case:

We have $|\psi_{t}\rangle$ defined as a tensor product (the result of the first phase of the quantum circuit, and the LHS of Nielsen & Chuang's identity 5.20 on pg 222):

In [8]:
_psi_t_def
 ⊢  
In [9]:
_psi_t_as_tensor_prod = _psi_t_def.instantiate()
_psi_t_as_tensor_prod:  ⊢  

For $\psi'_{1}$, we prove a useful equality then instantiate the psi_t_def with $t=1$:

In [10]:
psi_1_def = _psi_t_def.instantiate({t:one})
psi_1_def:  ⊢  

Then show that the summation formula also gives the same qbit result

In [11]:
sum_0_to_1 = base_case.rhs
sum_0_to_1:
In [12]:
sum_0_to_1_processed_01 = sum_0_to_1.inner_expr().operands[1].partitioning_first()
sum_0_to_1_processed_01:  ⊢  
In [13]:
# finish off the Base Case
base_case_jdgmt = sum_0_to_1_processed_01.sub_left_side_into(psi_1_def)
base_case_jdgmt:  ⊢  

Inductive Step

In [14]:
inductive_step = induction_inst.antecedent.operands[1]
inductive_step:
In [15]:
defaults.assumptions = defaults.assumptions + inductive_step.conditions.entries
defaults.assumptions:

First, partition the summation: $\sum_{k=0}^{2^{t+1}-1} e^{2\pi i \varphi k} |k\rangle_{t+1} = \sum_{k=0}^{2^{t}-1} e^{2\pi i \varphi k} |k\rangle_{t+1} + \sum_{k=2^{t}}^{2^{t+1}-1} e^{2\pi i \varphi k} |k\rangle_{t+1}$

In [16]:
desired_domain = _psi_t_formula.instance_expr.rhs.scaled.domain
desired_domain:
In [17]:
summation_partition_01 = (
    inductive_step.instance_expr.rhs.operands[1]
    .partitioning(desired_domain.upper_bound))
summation_partition_01:  ⊢  

Then shift the second summation of that partition, so that the two summations then have the same index domain:

In [18]:
summation_partition_02 = (summation_partition_01.inner_expr().rhs.
                          operands[1].shift(Neg(Exp(two, t))))
summation_partition_02:  ⊢  

We want to rewrite the summand of that 2nd summation on the rhs now by (1) expanding the exponential term and (2) rewriting the $|k+2^t{\rangle}_{t+1}$ ket as $|1\rangle \otimes |k{\rangle}_t$. This takes a little work.

In [19]:
rhs_2nd_sum = summation_partition_02.rhs.operands[1]
rhs_2nd_sum:
In [20]:
summand_processed_01 = rhs_2nd_sum.summand.inner_expr().operands[0].exponent.distribution(
    4, assumptions=[*defaults.assumptions,
                    rhs_2nd_sum.condition])
summand_processed_01: ,  ⊢  
In [21]:
summand_processed_02 = (
    summand_processed_01.inner_expr().rhs.operands[0]
    .exponent_separate(
        assumptions=[*defaults.assumptions,
                     InSet(k, Interval(zero, subtract(Exp(two, t), one)))]))
summand_processed_02: ,  ⊢  
In [22]:
# Avoid recombining these via auto-simplification
defaults.preserved_exprs = set([summand_processed_02.rhs.scalar])
defaults.preserved_exprs:
In [23]:
from proveit.physics.quantum.algebra import prepend_num_ket_with_one_ket
prepend_num_ket_with_one_ket
 ⊢  
In [24]:
prepend_num_ket_with_one_ket_inst = prepend_num_ket_with_one_ket.instantiate(
        {n: t, k: k},
        assumptions=[*defaults.assumptions, InSet(k, Interval(zero, subtract(Exp(two, t), one)))])
prepend_num_ket_with_one_ket_inst: ,  ⊢  
In [25]:
summand_processed_03 = (
    summand_processed_02.inner_expr().rhs.operands[1]
    .substitute(prepend_num_ket_with_one_ket_inst))
summand_processed_03: ,  ⊢  
In [26]:
# reminder of summation_partition_03
summation_partition_02
 ⊢  
In [27]:
summation_partition_04 = (
    summation_partition_02.inner_expr().rhs.operands[1].summand.substitute(
        summand_processed_03))
summation_partition_04:  ⊢  

Also process the summand in the 1st sum on the rhs, converting the ket $|k\rangle_{t+1}$ to the tensor product $|0\rangle \otimes |k\rangle_{t}$:

In [28]:
# pull up the relevant NumKet theorem
from proveit.physics.quantum.algebra import prepend_num_ket_with_zero_ket
prepend_num_ket_with_zero_ket
 ⊢  
In [29]:
# instantiate the theorem for our specific case
prepend_num_ket_with_zero_ket_inst = prepend_num_ket_with_zero_ket.instantiate(
        {n: t, k: k},
        assumptions=[*defaults.assumptions, InSet(k, Interval(zero, subtract(Exp(two, t), one)))])
prepend_num_ket_with_zero_ket_inst: ,  ⊢  
In [30]:
# use our instantiation to substitute
summation_partition_05 = (
    summation_partition_04.inner_expr().rhs.operands[0].summand.scaled.substitute(
    prepend_num_ket_with_zero_ket_inst))
summation_partition_05:  ⊢  
In [31]:
coef = inductive_step.instance_expr.rhs.scalar
summation_partition_06 = summation_partition_05.scalar_mult_both_sides(coef)
summation_partition_06:  ⊢  
In [32]:
# Recall our inductive hypothesis:
inductive_hypothesis = defaults.assumptions[-1]
inductive_hypothesis:
In [33]:
conclusion_01 = summation_partition_06.inner_expr().rhs.factor(
        inductive_hypothesis.rhs, pull='right', field=Complex)
conclusion_01:  ⊢  
In [34]:
# use the inductive hypothesis:
conclusion_02 = inductive_hypothesis.sub_left_side_into(conclusion_01)
conclusion_02: ,  ⊢  

The RHS of conclusion02 above should be equal to $|\psi{t+1}\rangle$. Let's see how to get there. Ideally we could use the next three cells to show the rhs of the equality in `conclusion_02` is equal to $|\psi_{t+1}\rangle$

In [35]:
# reminder
_psi_t_def
 ⊢  
In [36]:
psi_t_plus_one_as_tensor_prod = _psi_t_def.instantiate({t:Add(t, one)})
psi_t_plus_one_as_tensor_prod:  ⊢  

Now this substitute() step will also manage to pull the scalar coefficients out to the front in the process:

In [37]:
conclusion_03 = conclusion_02.inner_expr().rhs.operands[1].substitute(
        _psi_t_as_tensor_prod)
conclusion_03: ,  ⊢  

Now we partition the tensor product expression of $\psi_{t+1}$, so we can eventually show that it is equal to the rhs of conclusion_03.

In [38]:
psi_t_plus_one_as_tensor_prod.rhs
In [39]:
# # we can partition the operands in the psi_{t+1} tensor prod expression
psi_t_plus_one_as_tensor_prod_02 = (
    psi_t_plus_one_as_tensor_prod.inner_expr().rhs.operands[0].split(t))
psi_t_plus_one_as_tensor_prod_02:  ⊢  
In [40]:
conclusion_03.inner_expr().rhs.substitute(psi_t_plus_one_as_tensor_prod_02.derive_reversed())
,  ⊢  
In [41]:
# # recall our earlier instantiation of the induction theorem:
induction_inst
 ⊢  

We have proven both pieces of the antecedent (i.e., the base case and inductive case) of the instantiated induction theorem induction_inst, so we can now derive the consequent:

In [42]:
induction_inst.derive_consequent()
 ⊢   
_psi_t_formula has been proven.  Now simply execute "%qed".
In [43]:
%qed

proveit.physics.quantum.QPE._psi_t_formula has been proven.
Out[43]:
 step typerequirementsstatement
0modus ponens1, 2  ⊢  
1instantiation3, 4*, 5*, 6*  ⊢  
  : , : , :
2instantiation7, 8, 9  ⊢  
  : , :
3conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos
4instantiation603, 10, 450  ⊢  
  : , : , :
5instantiation11, 12  ⊢  
  :
6instantiation603, 13, 14  ⊢  
  : , : , :
7theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
8instantiation428, 15, 16  ⊢  
  : , : , :
9generalization17  ⊢  
10instantiation617, 632  ⊢  
  : , : , :
11conjecture  ⊢  
 proveit.physics.quantum.algebra.single_qubit_num_ket
12instantiation18, 19, 20  ⊢  
  :
13instantiation617, 126  ⊢  
  : , : , :
14instantiation462, 21  ⊢  
  : , :
15instantiation102, 681, 22, 23*  ⊢  
  :
16instantiation617, 24  ⊢  
  : , : , :
17instantiation462, 25,  ⊢  
  : , :
18conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonneg_int_is_natural
19instantiation684, 26, 28  ⊢  
  : , : , :
20instantiation27, 638, 665, 28  ⊢  
  : , : , :
21instantiation29, 646, 681, 673, 632*  ⊢  
  : , : , :
22instantiation545, 30, 31  ⊢  
  : , : , :
23instantiation603, 32, 33  ⊢  
  : , : , :
24instantiation34, 638, 665, 35, 36*, 37*  ⊢  
  : , : , : , :
25instantiation545, 38, 39,  ⊢  
  : , : , :
26instantiation637, 638, 665  ⊢  
  : , :
27conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
28assumption  ⊢  
29conjecture  ⊢  
 proveit.numbers.exponentiation.product_of_posnat_powers
30instantiation479, 345, 615, 298  ⊢  
  : , : , :
31instantiation494, 615, 577  ⊢  
  : , :
32instantiation617, 40  ⊢  
  : , : , :
33instantiation41, 487, 42  ⊢  
  : , : , :
34conjecture  ⊢  
 proveit.linear_algebra.addition.vec_sum_split_first
35conjecture  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
36instantiation603, 43, 44  ⊢  
  : , : , :
37instantiation603, 45, 46  ⊢  
  : , : , :
38instantiation545, 47, 48, 49*,  ⊢  
  : , : , :
39instantiation603, 50, 51  ⊢  
  : , : , :
40instantiation52, 681, 53  ⊢  
  : , : , :
41axiom  ⊢  
 proveit.linear_algebra.tensors.unary_tensor_prod_def
42instantiation455, 487, 203, 54  ⊢  
  : , : , : , :
43instantiation617, 55  ⊢  
  : , : , :
44instantiation56, 615, 324, 487  ⊢  
  : , : , :
45instantiation617, 57  ⊢  
  : , : , :
46instantiation58, 665, 59*  ⊢  
  : , :
47instantiation428, 60, 61,  ⊢  
  : , : , :
48instantiation102, 673  ⊢  
  :
49instantiation603, 62, 63  ⊢  
  : , : , :
50instantiation462, 64  ⊢  
  : , :
51instantiation462, 65  ⊢  
  : , :
52conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_eq_via_elem_eq
53instantiation617, 66  ⊢  
  : , : , :
54instantiation323, 487, 324, 67  ⊢  
  : , : , : , :
55instantiation603, 68, 69  ⊢  
  : , : , :
56conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.one_as_scalar_mult_id
57modus ponens70, 71  ⊢  
58axiom  ⊢  
 proveit.linear_algebra.addition.vec_sum_single
59instantiation593, 422, 612, 423, 614, 646, 569, 582, 583  ⊢  
  : , : , : , :
60instantiation545, 72, 73  ⊢  
  : , : , :
61assumption  ⊢  
62instantiation74, 674, 194, 612, 164, 106, 614, 487, 107, 108, 75, 110  ⊢  
  : , : , : , : , : , : , : , : , : , :
63instantiation458, 281, 612, 194, 614, 164, 106, 487, 107, 108, 278, 110  ⊢  
  : , : , : , : , : , : , : , : , : , :
64instantiation76, 686, 77, 78, 79, 80  ⊢  
  : , : , : , :
65instantiation81, 158, 82, 83, 84, 85, 86*  ⊢  
  : , : , : , :
66instantiation617, 87  ⊢  
  : , : , :
67instantiation455, 487, 88, 490  ⊢  
  : , : , : , :
68instantiation617, 89  ⊢  
  : , : , :
69instantiation301, 492  ⊢  
  :
70instantiation90, 681  ⊢  
  : , : , : , : , : , :
71generalization91  ⊢  
72instantiation92, 93  ⊢  
  : , : , :
73instantiation603, 94, 95  ⊢  
  : , : , :
74conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_disassociation
75instantiation455, 487, 281, 278  ⊢  
  : , : , : , :
76axiom  ⊢  
 proveit.core_expr_types.operations.operands_substitution
77instantiation626  ⊢  
  : , :
78instantiation626  ⊢  
  : , :
79instantiation462, 438  ⊢  
  : , :
80instantiation617, 96  ⊢  
  : , : , :
81conjecture  ⊢  
 proveit.logic.equality.sub_in_right_operands_via_tuple
82instantiation283, 97, 98, 101  ⊢  
  :