In [1]:
import proveit
from proveit import defaults, ExprTuple, ExprRange
from proveit import k, m, s, t, U
from proveit.numbers import (
Mult, Exp, zero, one, two, subtract, exp2pi_i)
from proveit.linear_algebra import MatrixExp, TensorProd
from proveit.physics.quantum import var_ket_u, varphi
from proveit.physics.quantum.circuits import (
QcircuitEquiv, phase_kickbacks_on_register)
from proveit.physics.quantum.QPE import (
_s, _t, _ket_u, _U, _phase, _s_in_nat_pos, _u_ket_register,
_normalized_ket_u, _unitary_U, _phase_in_interval, _eigen_uu,
QPE1_def, _psi_t_def, _psi_t_ket_is_normalized_vec)
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving _psi_t_output
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_psi_t_output:
(see dependencies)
_psi_t_output:
(see dependencies)
In [3]:
_psi_t_output
In [4]:
defaults.assumptions = _psi_t_output.conditions
defaults.assumptions: 
In [5]:
# don't combine factors of 2
Mult.change_simplification_directives(combine_all_exponents=False,
combine_numeric_rational_exponents=False)
In [6]:
_psi_t_def
In [7]:
_psi_t = _psi_t_def.instantiate()
_psi_t: 
⊢ 
⊢ 
In [8]:
_psi_t_ket_is_normalized_vec
In [9]:
_psi_t_ket_is_normalized_vec.instantiate()
In [10]:
target_circuit = _psi_t_output.instance_expr.lhs.operand
target_circuit: 
In [11]:
QPE1_def
In [12]:
QPE1_inst = QPE1_def.instantiate({s:_s, U:_U})
QPE1_inst: ⊢ 
⊢ 
In [13]:
phase_kickbacks_on_register
In [14]:
Uexponentials = ExprTuple(ExprRange(k, MatrixExp(_U, Exp(two, k)),
subtract(t, one), zero, order='decreasing'))
Uexponentials: 
In [15]:
phases = ExprTuple(ExprRange(k, Mult(Exp(two, k), _phase),
subtract(t, one), zero, order='decreasing'))
phases: 
In [16]:
kickbacks = phase_kickbacks_on_register.instantiate(
{m:_s, U:Uexponentials, var_ket_u:_ket_u, varphi:phases})
kickbacks: ⊢ 
⊢ 
In [17]:
kickbacks_with_QPE1 = QPE1_inst.sub_left_side_into(
kickbacks.inner_expr().lhs.operand)
kickbacks_with_QPE1: ⊢ 
⊢ 
For psi_t_tensor_u_expansion to simplify properly, we need to specify this default vector-space field, but we should be able to automate this in the future:
In [18]:
from proveit.numbers import Complex
from proveit.linear_algebra import VecSpaces
VecSpaces.default_field = Complex
VecSpaces.default_field: 
In [19]:
psi_t_tensor_u__expansion = _psi_t.substitution(TensorProd(_psi_t.lhs, _ket_u))
psi_t_tensor_u__expansion: ⊢ 
⊢ 
In [20]:
output_consolidation = kickbacks_with_QPE1.lhs.operand.output_consolidation(
replacements=[psi_t_tensor_u__expansion.derive_reversed()])
output_consolidation: ⊢ 
⊢ 
In [21]:
output_consolidation_from_desired = _psi_t_output.instance_expr.lhs.operand.output_consolidation()
output_consolidation_from_desired: ⊢ 
⊢ 
In [22]:
equiv = output_consolidation.apply_transitivity(output_consolidation_from_desired)
equiv: ⊢ 
⊢ 
In [23]:
equiv.sub_right_side_into(kickbacks_with_QPE1)
In [24]:
%qed
Out[24]:
| step type | requirements | statement | ||
|---|---|---|---|---|
| 0 | generalization | 1 | ⊢ | |
| 1 | instantiation | 4, 2, 3 | ⊢  | |
 :  ,  :  ,  : | ||||
| 2 | instantiation | 4, 5, 6 | ⊢ | |
 :  , :  , : | ||||
| 3 | instantiation | 7, 8, 9 | ⊢ | |
: , :  ,  : | ||||
| 4 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.rhs_prob_via_equiv | ||||
| 5 | instantiation | 10, 465, 753, 11, 12, 303, 13, 14, 15, 746, 748, 272, 16* | ⊢ | |
 :  ,  : ,  : ,  : ,  : | ||||
| 6 | modus ponens | 17, 18 | ⊢  | |
| 7 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.equiv_transitivity | ||||
| 8 | modus ponens | 19, 20 | ⊢  | |
| 9 | instantiation | 31, 21 | ⊢  | |
| : , : | ||||
| 10 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.phase_kickbacks_on_register | ||||
| 11 | instantiation | 603, 22, 653, 360 | ⊢  | |
 :  ,  : ,  : ,  :  | ||||
| 12 | modus ponens | 23, 24 | ⊢  | |
| 13 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._normalized_ket_u | ||||
| 14 | instantiation | 603, 25, 653, 360 | ⊢  | |
:  , : , : , : | ||||
| 15 | modus ponens | 26, 27 | ⊢  | |
| 16 | instantiation | 690, 676, 738, 691, 28, 29, 692, 714, 695, 704, 705, 694 | ,  ⊢  | |
 :  ,  :  ,  :  , :  , :  , :  | ||||
| 17 | instantiation | 47, 750, 471, 30 | ⊢  | |
:  , : ,  : , : , :  , :  , :  ,  :  | ||||
| 18 | instantiation | 31, 32 | ⊢  | |
:  , :  | ||||
| 19 | instantiation | 47, 738, 750, 691, 48, 692 | ⊢  | |
: , : , : , : , :  , : , : , :  | ||||
| 20 | instantiation | 672, 33, 34 | ⊢  | |
 :  ,  :  ,  :  | ||||
| 21 | modus ponens | 35, 36 | ⊢  | |
| 22 | instantiation | 672, 37, 417 | ⊢  | |
:  , :  , : | ||||
| 23 | instantiation | 419, 742, 743, 420 | ⊢  | |
:  , : ,  :  , :  | ||||
| 24 | generalization | 38 | ⊢  | |
| 25 | instantiation | 672, 39, 417 | ⊢  | |
:  , : , : | ||||
| 26 | instantiation | 419, 742, 743, 420 | ⊢  | |
: , : , :  , : | ||||
| 27 | generalization | 40 | ⊢  | |
| 28 | instantiation | 696 | ⊢  | |
: , :  , :  | ||||
| 29 | instantiation | 706 | ⊢  | |
:  , : | ||||
| 30 | instantiation | 603, 41, 653, 360 | ⊢  | |
:  , : , : , : | ||||
| 31 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.equiv_reversal | ||||
| 32 | instantiation | 42, 465, 753, 59 | ⊢ | |
| : , : , : | ||||
| 33 | instantiation | 672, 43, 44 | ⊢  | |
: , :  , : | ||||
| 34 | instantiation | 238, 471, 67, 45, 46 | ⊢  | |
 : ,  :  , :  , :  | ||||
| 35 | instantiation | 47, 738, 750, 691, 48, 692 | ⊢  | |
: , : , : , : , : , :  , : , : | ||||
| 36 | instantiation | 82, 656, 49, 753, 465, 50, 51, 303, 52, 53, 54, 55, 56, 270, 543, 691, 471, 96, 57, 555* | ⊢  | |
: , :  , :  ,  :  ,  : ,  : | ||||
| 37 | instantiation | 466, 467 | ⊢  | |
 :  , : , : | ||||
| 38 | instantiation | 58, 61, 358, 59 | , ⊢ | |
: , :  , : | ||||
| 39 | instantiation | 466, 467 | ⊢  | |
:  , : , : | ||||
| 40 | instantiation | 60, 61, 707, 62 | , ⊢ | |
: ,  : , : , : | ||||
| 41 | instantiation | 672, 63, 417 | ⊢  | |
 :  , : , : | ||||
| 42 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE.QPE1_def | ||||
| 43 | instantiation | 672, 64, 65 | ⊢  | |
:  , :  , :  | ||||
| 44 | instantiation | 238, 471, 66, 67, 68 | ⊢  | |
: , : , :  , : | ||||
| 45 | instantiation | 69, 471 | ⊢  | |
: , :  | ||||
| 46 | instantiation | 394, 745, 327, 328, 329, 330* | ⊢  | |
:  , :  , : , : , : , : | ||||
| 47 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.circuit_equiv_temporal_sub | ||||
| 48 | instantiation | 706 | ⊢  | |
:  , :  | ||||
| 49 | instantiation | 706 | ⊢  | |
| : , : | ||||
| 50 | instantiation | 706 | ⊢  | |
:  , : | ||||
| 51 | instantiation | 70, 71 | ⊢  | |
: , :  | ||||
| 52 | instantiation | 603, 72, 73, 74 | ⊢  | |
:  , : , : , :  | ||||
| 53 | instantiation | 613, 75 | ⊢  | |
:  , : | ||||
| 54 | instantiation | 706 | ⊢  | |
: , :  | ||||
| 55 | instantiation | 613, 76 | ⊢  | |
: , :  | ||||
| 56 | instantiation | 603, 77, 579, 78 | ⊢  | |
:  , : , : , :  | ||||
| 57 | instantiation | 181, 676, 79, 184, 80, 186 | ⊢  | |
: , :  | ||||
| 58 | conjecture | ⊢  | ||
| proveit.linear_algebra.matrices.exponentiation.U_closure | ||||
| 59 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._unitary_U | ||||
| 60 | conjecture | ⊢  | ||
| proveit.linear_algebra.matrices.exponentiation.unital2pi_eigen_exp_application | ||||
| 61 | instantiation | 414, 738, 81 | , ⊢  | |
: , :  | ||||
| 62 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._eigen_uu | ||||
| 63 | instantiation | 466, 467 | ⊢  | |
 :  , : , : | ||||
| 64 | instantiation | 82, 433, 83, 654, 84, 465, 85, 86, 87, 303, 88, 89, 90, 91, 92, 93, 94, 270, 169, 691, 95, 96, 97, 555, 98, 99*, 100*, 101* | ⊢  | |
:  , :  , :  , :  ,  :  ,  :  | ||||
| 65 | instantiation | 238, 471, 102, 103, 104 | ⊢  | |
| : | ||||