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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, x
from proveit.logic import InSet
from proveit.numbers import (zero, one, two, five, Add, Exp, frac, greater,
Integer, Neg, Real, RealPos, subtract)
# QPE common expressions
from proveit.physics.quantum.QPE import _t, _n
# QPE axioms
from proveit.physics.quantum.QPE import (
_eps_in_interval, _n_in_natural_pos, _t_in_natural_pos, _t_req)

In [2]:
%proving _e_value_ge_two

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_e_value_ge_two:
(see dependencies)
In [3]:
_t_in_natural_pos

In [4]:
_n_in_natural_pos

In [5]:
_eps_in_interval

In [6]:
_t_req

In [7]:
bound_01 = _t_req.right_add_both_sides(Neg(_n))

bound_01:
In [8]:
_eps_le_one = _eps_in_interval.derive_element_upper_bound()

_eps_le_one:
In [9]:
bound_02 = bound_01.rhs.deduce_bound(_eps_le_one)

bound_02:
In [10]:
bound_03 = bound_01.apply_transitivity(bound_02)

bound_03:

Note that ${\rm log}_2(x) > 1$ if $x > 2$:

In [11]:
bound_04 = bound_03.rhs.deduce_bound(greater(frac(five, two), two))

bound_04:
In [12]:
bound_05 = bound_03.apply_transitivity(bound_04)

bound_05:
In [13]:
bound_06 = Exp(two, subtract(_t, _n)).deduce_bound(bound_05)

bound_06:
_e_value_ge_two may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [14]:
%qed

proveit.physics.quantum.QPE._e_value_ge_two has been proven.

Out[14]:
step typerequirementsstatement
0instantiation1, 2, 3, 4, 5, 6*, 7*
: , : , :
1reference88
2reference113
3reference17
4instantiation112, 26, 242
: , :
5instantiation55, 17, 26, 242, 8, 9
: , : , :
6instantiation10, 185, 11, 12
: , : , :
7instantiation172, 13, 14
: , : , :
8instantiation15, 196, 56, 222, 57, 16*
: , : , :
9instantiation184, 250
:
10conjecture
11instantiation248, 207, 17
: , : , :
12conjecture
13instantiation130, 131, 221, 250, 132, 18, 21, 199, 79
: , : , : , : , : , :
14instantiation19, 250, 221, 131, 20, 132, 21, 199, 79, 22*
: , : , : , : , : , :
15conjecture
proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
16instantiation65, 23, 24, 189
: , : , : , :
17instantiation248, 244, 25
: , : , :
18instantiation197
: , :
19conjecture
20instantiation197
: , :
21instantiation248, 207, 26
: , : , :
22instantiation27, 199, 185, 71
: , : , :
23instantiation28, 238, 185
: , :
24instantiation29, 221, 30, 31, 32
: , : , : , :
25instantiation248, 246, 33
: , : , :
26instantiation34, 196, 35
: , :
27conjecture
28conjecture
proveit.numbers.exponentiation.exp_nat_pos_expansion
29conjecture
proveit.core_expr_types.operations.operands_substitution_via_tuple
30instantiation36, 221
: , :
31instantiation197
: , :
32instantiation37
:
33instantiation248, 249, 38
: , : , :
34conjecture
proveit.numbers.exponentiation.exp_real_closure_nat_power
35instantiation39, 40, 41
:
36conjecture
proveit.core_expr_types.tuples.range_from1_len_typical_eq
37conjecture
proveit.numbers.numerals.decimals.reduce_2_repeats
38conjecture
proveit.numbers.numerals.decimals.nat4
39conjecture
proveit.numbers.number_sets.integers.nonneg_int_is_natural
40instantiation42, 43, 44
: , :
41instantiation45, 46
: , :
42conjecture
43instantiation248, 47, 139
: , : , :
44instantiation248, 48, 49
: , : , :
45conjecture
46instantiation88, 92, 196, 50, 51, 52*, 53*
: , : , :
47conjecture
proveit.numbers.number_sets.integers.nat_pos_within_int
48conjecture
proveit.numbers.number_sets.integers.neg_int_within_int
49instantiation54, 193
:
50instantiation112, 56, 196
: , :
51instantiation55, 196, 56, 57, 169
: , : , :
52instantiation172, 58, 59
: , : , :
53instantiation172, 60, 61
: , : , :
54conjecture
proveit.numbers.negation.int_neg_closure
55conjecture
56instantiation112, 114, 157
: , :
57instantiation72, 62, 63
: , : , :
58instantiation130, 250, 221, 131, 78, 132, 185, 136, 79
: , : , : , : , : , :
59instantiation135, 185, 136, 97
: , : , :
60instantiation144, 64
: , : , :
61instantiation65, 66, 67, 68
: , : , : , :
62instantiation69, 247, 86, 70, 71*
: , :
63instantiation72, 73, 74
: , : , :
64instantiation130, 131, 221, 250, 132, 96, 99, 134, 185
: , : , : , : , : , :
65conjecture
proveit.logic.equality.four_chain_transitivity
66instantiation130, 131, 76, 250, 132, 77, 99, 134, 185, 75
: , : , : , : , : , :
67instantiation130, 76, 221, 131, 77, 78, 132, 99, 134, 185, 136, 79
: , : , : , : , : , :
68instantiation172, 80, 81
: , : , :
69conjecture
proveit.numbers.rounding.ceil_of_real_above_int
70instantiation82, 230, 108, 83, 222, 84*
: , : , :
71conjecture
72conjecture
proveit.numbers.ordering.transitivity_less_eq_less_eq
73instantiation85, 86, 203, 87
: , :
74instantiation88, 157, 89, 114, 90, 91*
: , : , :
75instantiation248, 207, 92
: , : , :
76conjecture
proveit.numbers.numerals.decimals.nat3
77instantiation93
: , : , :
78instantiation197
: , :
79instantiation94, 185
:
80instantiation95, 221, 250, 131, 96, 132, 99, 134, 185, 136, 97
: , : , : , : , : , : , : , :
81instantiation98, 136, 99, 138
: , : , :
82conjecture
proveit.numbers.logarithms.log_increasing_less
83instantiation100, 196, 101, 102, 103, 104*, 105*
: , : , :
84instantiation106, 230
:
85conjecture
proveit.numbers.rounding.ceil_increasing_less_eq
86instantiation208, 230, 108, 210
: , :
87instantiation107, 230, 108, 209, 109, 222
: , : , :
88conjecture
89instantiation112, 177, 158
: , :
90axiom
proveit.physics.quantum.QPE._t_req
91instantiation172, 110, 111
: , : , :
92instantiation112, 177, 113
: , :
93conjecture
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
94conjecture
proveit.numbers.negation.complex_closure
95conjecture
96instantiation197
: , :
97instantiation159
:
98conjecture
99instantiation248, 207, 114
: , : , :
100conjecture
101instantiation115, 179, 241
: , :
102instantiation248, 244, 116
: , : , :
103instantiation117, 179, 241, 242, 118, 119
: , : , :
104instantiation172, 120, 121
: , : , :
105instantiation172, 122, 123
: , : , :
106conjecture
proveit.numbers.logarithms.log_eq_1
107conjecture
proveit.numbers.logarithms.log_increasing_less_eq
108instantiation217, 124, 230, 125
: , :
109instantiation126, 196, 179, 127, 128, 129*
: , : , :
110instantiation130, 131, 221, 250, 132, 133, 136, 137, 134
: , : , : , : , : , :
111instantiation135, 136, 137, 138
: , : , :
112conjecture
113instantiation176, 196
:
114instantiation191, 192, 139
: , : , :
115conjecture
proveit.numbers.multiplication.mult_real_closure_bin
116instantiation140, 195, 245
: , :
117conjecture
proveit.numbers.multiplication.strong_bound_via_right_factor_bound
118conjecture
proveit.numbers.numerals.decimals.less_0_1
119instantiation141, 205
:
120instantiation144, 142
: , : , :
121instantiation143, 185
:
122instantiation144, 145
: , : , :
123instantiation153, 247, 212, 154*, 146*, 170*
: , : , : , :
124instantiation248, 232, 147
: , : , :
125instantiation148, 238
:
126conjecture
127instantiation248, 149, 214
: , : , :
128instantiation150, 151, 228, 230, 152
: , : , :
129instantiation153, 212, 247, 154*, 155*, 156*
: , : , : , :
130conjecture
131axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
132conjecture
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
133instantiation197
: , :
134instantiation248, 207, 157
: , : , :
135conjecture
136instantiation248, 207, 177
: , : , :
137instantiation248, 207, 158
: , : , :
138instantiation159
:
139axiom
proveit.physics.quantum.QPE._t_in_natural_pos
140conjecture
proveit.numbers.multiplication.mult_rational_closure_bin
141conjecture
proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
142instantiation160, 161
:
143conjecture
144axiom
proveit.logic.equality.substitution
145instantiation198, 161
:
146instantiation172, 162, 163
: , : , :
147instantiation248, 237, 164
: , : , :
148conjecture
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
149conjecture
proveit.numbers.number_sets.real_numbers.real_pos_within_real
150conjecture
proveit.numbers.division.weak_div_from_denom_bound__all_pos
151instantiation248, 165, 166
: , : , :
152instantiation167, 196, 235, 242, 168, 169, 170*
: , : , :
153conjecture
154instantiation171, 185
:
155instantiation172, 173, 174
: , : , :
156instantiation175, 185
:
157instantiation176, 177
:
158instantiation248, 244, 178
: , : , :
159axiom
proveit.logic.equality.equals_reflexivity
160conjecture
proveit.numbers.multiplication.mult_zero_right
161instantiation248, 207, 179
: , : , :
162instantiation186, 221, 180, 181, 190, 189
: , : , : , :
163conjecture
164conjecture
proveit.numbers.numerals.decimals.posnat5
165conjecture
proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
166instantiation248, 182, 250
: , : , :
167conjecture
proveit.numbers.multiplication.weak_bound_via_right_factor_bound
168instantiation183, 241, 242, 243
: , : , :
169instantiation184, 221
:
170instantiation198, 185
:
171conjecture
proveit.numbers.division.frac_one_denom
172axiom
proveit.logic.equality.equals_transitivity
173instantiation186, 221, 187, 188, 189, 190
: , : , : , :
174conjecture
175conjecture
proveit.numbers.multiplication.elim_one_left
176conjecture
proveit.numbers.negation.real_closure
177instantiation191, 192, 193
: , : , :
178instantiation248, 246, 194
: , : , :
179instantiation248, 244, 195
: , : , :
180instantiation197
: , :
181instantiation197
: , :
182conjecture
proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
183conjecture
proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound
184conjecture
proveit.numbers.number_sets.natural_numbers.natural_lower_bound
185instantiation248, 207, 196
: , : , :
186axiom
proveit.core_expr_types.operations.operands_substitution
187instantiation197
: , :
188instantiation197
: , :
189conjecture
proveit.numbers.numerals.decimals.mult_2_2
190instantiation198, 199
:
191theorem
proveit.logic.sets.inclusion.unfold_subset_eq
192instantiation200, 201
: , :
193axiom
proveit.physics.quantum.QPE._n_in_natural_pos
194instantiation202, 203
:
195instantiation248, 204, 205
: , : , :
196instantiation248, 244, 206
: , : , :
197conjecture
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
198conjecture
proveit.numbers.multiplication.elim_one_right
199instantiation248, 207, 242
: , : , :
200theorem
proveit.logic.sets.inclusion.relax_proper_subset
201conjecture
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
202axiom
proveit.numbers.rounding.ceil_is_an_int
203instantiation208, 230, 209, 210
: , :
204conjecture
proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
205instantiation211, 223, 233
: , :
206instantiation248, 246, 212
: , : , :
207conjecture
proveit.numbers.number_sets.complex_numbers.real_within_complex
208conjecture
proveit.numbers.logarithms.log_real_pos_real_closure
209instantiation213, 230, 214
: , :
210instantiation215, 216
: , :
211conjecture
proveit.numbers.division.div_rational_pos_closure
212instantiation248, 249, 221
: , : , :
213conjecture
214instantiation217, 218, 228, 219
: , :
215theorem
proveit.logic.equality.not_equals_symmetry
216instantiation220, 250, 221, 222
: , :
217conjecture
proveit.numbers.division.div_real_pos_closure
218instantiation248, 232, 223
: , : , :
219instantiation224, 225
:
220conjecture
proveit.numbers.ordering.less_is_not_eq_nat
221conjecture
proveit.numbers.numerals.decimals.nat2
222conjecture
proveit.numbers.numerals.decimals.less_1_2
223instantiation248, 237, 226
: , : , :
224conjecture
proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
225instantiation248, 227, 228
: , : , :
226conjecture
proveit.numbers.numerals.decimals.posnat1
227conjecture
proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
228instantiation229, 230, 231
: , :
229conjecture
proveit.numbers.multiplication.mult_real_pos_closure_bin
230instantiation248, 232, 233
: , : , :
231instantiation234, 235, 236
:
232conjecture
proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
233instantiation248, 237, 238
: , : , :
234conjecture
proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
235instantiation239, 241, 242, 243
: , : , :
236instantiation240, 241, 242, 243
: , : , :
237conjecture
proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
238conjecture
proveit.numbers.numerals.decimals.posnat2
239conjecture
proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
240conjecture
proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
241conjecture
proveit.numbers.number_sets.real_numbers.zero_is_real
242instantiation248, 244, 245
: , : , :
243axiom
proveit.physics.quantum.QPE._eps_in_interval
244conjecture
proveit.numbers.number_sets.real_numbers.rational_within_real
245instantiation248, 246, 247
: , : , :
246conjecture
proveit.numbers.number_sets.rational_numbers.int_within_rational
247instantiation248, 249, 250
: , : , :
248theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
249conjecture
proveit.numbers.number_sets.integers.nat_within_int
250theorem
proveit.numbers.numerals.decimals.nat1
*equality replacement requirements