logo
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  ⊢  
 proveit.linear_algebra.addition.norm_of_sum_of_orthogonal_pair
72instantiation261, 100, 101,  ⊢  
  : , : , :
73instantiation102, 134, 186, 136, 103*,  ⊢  
  : , : , : , :
74instantiation235, 104  ⊢  
  : , : , :
75instantiation261, 105, 106  ⊢  
  : , : , :
76instantiation107, 108, 109, 110  ⊢  
  : , : , : , :
77conjecture  ⊢  
 proveit.numbers.addition.add_nat_closure_bin
78instantiation326, 111, 112  ⊢  
  : , : , :
79instantiation253, 113, 114  ⊢  
  : , : , :
80instantiation253, 115, 116  ⊢  
  : , : , :
81conjecture  ⊢  
 proveit.numbers.addition.add_nat_closure
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  ⊢  
 proveit.linear_algebra.addition.binary_closure
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  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_32
123instantiation224  ⊢  
  :
124conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
125conjecture  ⊢  
 proveit.numbers.addition.elim_zero_any
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  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
143conjecture  ⊢  
 proveit.numbers.division.mult_frac_cancel_denom_left
144instantiation326, 171, 170  ⊢  
  : , : , :
145instantiation326, 171, 184  ⊢  
  : , : , :
146instantiation235, 172  ⊢  
  : , : , :
147instantiation235, 173  ⊢  
  : , : , :
148instantiation220, 200  ⊢  
  :
149conjecture  ⊢  
 proveit.numbers.addition.add_nat_pos_from_nonneg
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  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_12
156conjecture  ⊢  
 proveit.numbers.addition.elim_zero_left
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  ⊢  
 proveit.numbers.addition.disassociation
175instantiation290  ⊢  
  : , :
176conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_31
177conjecture  ⊢  
 proveit.numbers.negation.double_negation
178conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
179instantiation198, 328  ⊢  
  :
180instantiation199, 200, 201  ⊢  
  : , :
181instantiation202, 203, 204  ⊢  
  : , :
182instantiation326, 259, 239  ⊢  
  : , : , :
183conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
184instantiation326, 205, 206  ⊢  
  : , :