# Proof of proveit.physics.quantum.QPE._psi_t_ket_is_normalized_vec theorem¶

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import defaults
from proveit.logic import InSet
from proveit.numbers import Mult, Complex
from proveit.physics.quantum.QPE import _psi_t_def, _phase_is_real
In [2]:
%proving _psi_t_ket_is_normalized_vec
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_psi_t_ket_is_normalized_vec:
(see dependencies)
In [3]:
defaults.assumptions = _psi_t_ket_is_normalized_vec.conditions
defaults.assumptions:

Keep the $2$ in $2 \pi i ...$ from combining with the other factors of $2$:

In [4]:
Mult.change_simplification_directives(combine_all_exponents=False)
In [5]:
psi_t_def_inst = _psi_t_def.instantiate()
psi_t_def_inst:
In [6]:
psi_t_def_inst.rhs.compute_norm(field=Complex, replacements=[psi_t_def_inst.derive_reversed()])
In [7]:
domain = _psi_t_ket_is_normalized_vec.instance_expr.operands[0].domain
domain:
In [8]:
InSet(psi_t_def_inst.rhs, domain).prove()
In [9]:
%qed
proveit.physics.quantum.QPE._psi_t_ket_is_normalized_vec has been proven.
Out[9]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4
: , :
2theorem
proveit.logic.booleans.conjunction.and_if_both
3instantiation190, 5, 14
: , : , :
4instantiation6, 328, 20, 7, 22, 23, 8, 9*
: , : , : , :
5instantiation244, 10, 11
: , : , :
6conjecture
proveit.linear_algebra.tensors.norm_preserving_tensor_prod
7instantiation31, 317, 318, 134, 46
: , : , :
8modus ponens12, 13
9instantiation211, 14
: , :
10instantiation15, 328, 16, 17, 18*
: , : , :
11instantiation19, 328, 20, 21, 22, 23
: , : , : , :
12instantiation45, 317, 318, 46
: , : , : , :
13generalization24
14instantiation25, 328
:
15conjecture
proveit.linear_algebra.tensors.tensor_prod_of_cart_exps_within_cart_exp
16instantiation107, 26, 204, 33
: , : , : , :
17instantiation31, 317, 318, 260, 46
: , : , :
18instantiation27, 28, 297, 43, 29*, 43*
: , :
19conjecture
proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
20instantiation107, 30, 204, 33
: , : , : , :
21instantiation31, 317, 318, 130, 46
: , : , :
22instantiation107, 32, 204, 33
: , : , : , :
23modus ponens34, 35
24instantiation253, 36, 37,  ⊢
: , : , :
25axiom
proveit.physics.quantum.QPE._psi_t_def
26instantiation261, 38, 43
: , : , :
27conjecture
proveit.numbers.exponentiation.exp_nat_pos_rev
28instantiation149, 311, 278, 39, 279, 83, 325, 150
: , : , : , : , :
29instantiation211, 40
: , :
30instantiation261, 41, 43
: , : , :
31conjecture
proveit.logic.booleans.conjunction.redundant_conjunction_general
32instantiation261, 42, 43
: , : , :
33instantiation211, 44
: , :
34instantiation45, 317, 318, 46
: , : , : , :
35generalization47
36instantiation102, 134, 67, 68, 48*, 49*,  ⊢
: , : , : , :
37instantiation253, 50, 51
: , : , :
38instantiation56, 57
: , : , :
39instantiation290
: , :
40instantiation52, 320, 53, 54, 55
: , : , : , : , : , :
41instantiation56, 57
: , : , :
42instantiation56, 57
: , : , :
43instantiation253, 58, 59
: , : , :
44instantiation60, 61
: , :
45conjecture
proveit.logic.booleans.conjunction.conjunction_from_quantification
46instantiation178, 62, 63, 223, 64, 65*, 66*
: , : , :
47instantiation129, 130, 67, 68,  ⊢
: , : , : , :
48instantiation69, 70
:
49instantiation71, 130, 135, 97, 72, 73*,  ⊢
: , : , : , :
50instantiation235, 74
: , : , :
51instantiation261, 75, 76
: , : , :
52conjecture
proveit.core_expr_types.tuples.shift_equivalence
53instantiation77, 78, 83
: , :
54instantiation211, 79
: , :
55instantiation211, 80
: , :
56conjecture
proveit.core_expr_types.tuples.range_len
57instantiation81, 265, 82, 278, 83, 325
: , :
58instantiation235, 84
: , : , :
59instantiation107, 85, 86, 87
: , : , : , :
60conjecture
proveit.core_expr_types.tuples.range_from1_len
61instantiation326, 111, 328
: , : , :
62instantiation326, 309, 88
: , : , :
63conjecture
proveit.numbers.number_sets.real_numbers.zero_is_real
64instantiation89, 90
: , :
65instantiation253, 91, 92
: , : , :
66instantiation107, 93, 123, 94
: , : , : , :
67instantiation326, 306, 95
: , : , :
68instantiation96, 130, 135, 97,  ⊢
: , : , : , :
69conjecture
proveit.numbers.absolute_value.abs_non_neg_elim
70instantiation98, 99
:
71conjecture
72instantiation261, 100, 101,  ⊢
: , : , :
73instantiation102, 134, 186, 136, 103*,  ⊢
: , : , : , :
74instantiation235, 104
: , : , :
75instantiation261, 105, 106
: , : , :
76instantiation107, 108, 109, 110
: , : , : , :
77conjecture
78instantiation326, 111, 112
: , : , :
79instantiation253, 113, 114
: , : , :
80instantiation253, 115, 116
: , : , :
81conjecture
82instantiation283
: , : , :
83instantiation284, 117
:
84instantiation118, 201, 200, 153*
: , :
85instantiation174, 325, 311, 119, 164, 203, 121, 200
: , : , : , : , : , :
86instantiation125, 278, 265, 279, 120, 203, 121, 200
: , : , : , :
87instantiation122, 200, 203, 123
: , : , :
88instantiation326, 312, 317
: , : , :
89conjecture
proveit.numbers.ordering.relax_less
90instantiation124, 328
:
91instantiation174, 325, 311, 278, 175, 279, 164, 201, 200
: , : , : , : , : , :
92instantiation125, 278, 311, 279, 175, 201, 200
: , : , : , :
93instantiation253, 126, 127
: , : , :
94instantiation211, 128
: , :
95instantiation326, 299, 132
: , : , :
96conjecture
97instantiation129, 130, 186, 136,  ⊢
: , : , : , :
98conjecture
proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg
99instantiation326, 131, 132
: , : , :
100instantiation133, 134, 186, 135, 136,  ⊢
: , : , : , : , :
101instantiation253, 137, 138,  ⊢
: , : , :
102conjecture
proveit.linear_algebra.inner_products.scaled_norm
103instantiation253, 139, 140,  ⊢
: , : , :
104instantiation253, 141, 142
: , : , :
105instantiation143, 200, 144, 145
: , : , : , : , :
106instantiation253, 146, 147
: , : , :
107conjecture
proveit.logic.equality.four_chain_transitivity
108instantiation235, 148
: , : , :
109instantiation235, 148
: , : , :
110instantiation240, 200
:
111conjecture
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
112instantiation149, 325, 278, 279, 150
: , : , : , : , :
113instantiation235, 153
: , : , :
114instantiation253, 151, 152
: , : , :
115instantiation235, 153
: , : , :
116instantiation156, 203
:
117instantiation294, 317, 154
:
118conjecture
proveit.numbers.negation.distribute_neg_through_binary_sum
119instantiation290
: , :
120instantiation283
: , : , :
121instantiation303, 200
:
122conjecture
123instantiation224
:
124conjecture
proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
125conjecture
126instantiation174, 325, 311, 278, 175, 279, 203, 201, 200
: , : , : , : , : , :
127instantiation155, 203, 200, 204
: , : , :
128instantiation156, 200
:
129conjecture
proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
130instantiation157, 260
:
131conjecture
proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonneg
132instantiation158, 159, 206, 160
: , :
133conjecture
proveit.linear_algebra.inner_products.inner_prod_scalar_mult_right
134instantiation161, 260
:
135conjecture
proveit.physics.quantum.algebra.ket_zero_in_qubit_space
136conjecture
proveit.physics.quantum.algebra.ket_one_in_qubit_space
137instantiation235, 162
: , : , :
138instantiation163, 186, 164, 165*,  ⊢
: , :
139instantiation235, 166,  ⊢
: , : , :
140instantiation218, 167
:
141instantiation253, 168, 169
: , : , :
142conjecture
143conjecture
proveit.numbers.division.mult_frac_cancel_denom_left
144instantiation326, 171, 170
: , : , :
145instantiation326, 171, 184
: , : , :
146instantiation235, 172
: , : , :
147instantiation235, 173
: , : , :
148instantiation220, 200
:
149conjecture
150conjecture
proveit.numbers.numerals.decimals.less_0_1
151instantiation174, 278, 311, 325, 279, 175, 201, 200, 203
: , : , : , : , : , :
152instantiation176, 203, 200, 204
: , : , :
153instantiation177, 203
:
154instantiation178, 222, 221, 223, 179, 180*, 181*
: , : , :
155conjecture
156conjecture
157conjecture
proveit.linear_algebra.complex_vec_set_is_vec_space
158conjecture
proveit.numbers.division.div_real_pos_closure
159instantiation326, 246, 182
: , : , :
160instantiation183, 184
:
161conjecture
proveit.linear_algebra.inner_products.complex_vec_set_is_inner_prod_space
162conjecture
proveit.physics.quantum.algebra.ket_zero_and_one_have_zero_inner_prod
163axiom
proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
164conjecture
proveit.numbers.number_sets.complex_numbers.zero_is_complex
165instantiation185, 186,  ⊢
:
166instantiation187, 188, 189*,  ⊢
:
167instantiation190, 200, 236
: , : , :
168instantiation235, 191
: , : , :
169instantiation235, 192
: , : , :
170instantiation326, 193, 194
: , : , :
171conjecture
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
172instantiation235, 195
: , : , :
173instantiation253, 196, 197
: , : , :
174conjecture
175instantiation290
: , :
176conjecture
177conjecture
proveit.numbers.negation.double_negation
178conjecture