logo
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b # used in an instantiation dict
from proveit.numbers import (
        zero, one, two, Add, frac, greater, Integer, Mult,
        NaturalPos, Neg, Real, subtract)
from proveit.physics.quantum.QPE import (
        _e_domain, _eps_in_interval, _e_value, _e_value_ge_two,
        _n, _n_ge_two, _n_in_natural_pos, _t, _t_in_natural_pos, _t_req)
In [2]:
%proving _e_value_in_e_domain
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_e_value_in_e_domain:
(see dependencies)
In [3]:
_n_in_natural_pos
In [4]:
_t_in_natural_pos
In [5]:
_n_ge_two
In [6]:
_t_req
In [7]:
_eps_in_interval
In [8]:
bound_01 = _t_req.right_add_both_sides(Neg(_n))
bound_01:  ⊢  
In [9]:
_eps_le_one = _eps_in_interval.derive_element_upper_bound()
_eps_le_one:  ⊢  
In [10]:
greater(Add(two, frac(one, two)), zero).prove()
In [11]:
bound_02 = bound_01.rhs.deduce_bound(_eps_le_one)
bound_02:  ⊢  
In [12]:
bound_03 = bound_01.apply_transitivity(bound_02)
bound_03:  ⊢  
In [13]:
from proveit.numbers.logarithms import log_base_large_a_greater_one
log_base_large_a_greater_one
In [14]:
_a_sub, _b_sub = (
    bound_03.rhs.operand.base,
    bound_03.rhs.operand.antilog)
log_base_2_of_stuff_greater_than_one = log_base_large_a_greater_one.instantiate(
    {a: _a_sub, b: _b_sub})
log_base_2_of_stuff_greater_than_one:  ⊢  
In [15]:
bound_04 = bound_03.rhs.deduce_bound(log_base_2_of_stuff_greater_than_one)
bound_04:  ⊢  
In [16]:
bound_05 = bound_03.apply_transitivity(bound_04)
bound_05:  ⊢  
In [17]:
_e_value_ge_two
In [18]:
_n_ge_two
In [19]:
bound_06 = _e_value.deduce_bound(_n_ge_two)
bound_06:  ⊢  
In [20]:
bound_07 = bound_06.add_right(bound_06.rhs)
bound_07:  ⊢  
_e_value_in_e_domain may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [21]:
%qed
proveit.physics.quantum.QPE._e_value_in_e_domain has been proven.
Out[21]:
 step typerequirementsstatement
0instantiation1, 2, 3, 4, 5  ⊢  
  : , : , :
1conjecture  ⊢  
 proveit.numbers.number_sets.integers.in_interval
2reference316  ⊢  
3instantiation110, 6, 112  ⊢  
  : , :
4instantiation110, 7, 31  ⊢  
  : , :
5instantiation170, 8, 9  ⊢  
  : , :
6instantiation10, 280, 11  ⊢  
  : , :
7instantiation317, 116, 12  ⊢  
  : , : , :
8instantiation158, 90, 264, 13, 14, 15*, 16*  ⊢  
  : , : , :
9instantiation17, 18, 19  ⊢  
  : , : , :
10conjecture  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
11instantiation103, 20, 21  ⊢  
  :
12instantiation59, 290, 67  ⊢  
  : , :
13instantiation177, 26, 311  ⊢  
  : , :
14instantiation126, 264, 26, 311, 22, 23  ⊢  
  : , : , :
15instantiation24, 272, 251, 142  ⊢  
  : , : , :
16instantiation224, 25  ⊢  
  : , : , :
17theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
18instantiation126, 26, 60, 27, 28, 29*  ⊢  
  : , : , :
19instantiation224, 30  ⊢  
  : , : , :
20instantiation110, 111, 31  ⊢  
  : , :
21instantiation113, 32  ⊢  
  : , :
22conjecture  ⊢  
 proveit.physics.quantum.QPE._e_value_ge_two
23instantiation250, 319  ⊢  
  :
24conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add
25instantiation245, 33, 34  ⊢  
  : , : , :
26instantiation177, 57, 90  ⊢  
  : , :
27instantiation158, 90, 57, 92, 35  ⊢  
  : , : , :
28instantiation158, 90, 311, 92, 36, 37*  ⊢  
  : , : , :
29instantiation136, 38, 39, 40  ⊢  
  : , : , : , :
30instantiation224, 41  ⊢  
  : , : , :
31instantiation317, 117, 42  ⊢  
  : , : , :
32instantiation47, 200  ⊢  
  :
33instantiation191, 192, 290, 319, 193, 43, 44, 65, 272  ⊢  
  : , : , : , : , : , :
34instantiation168, 272, 44, 50  ⊢  
  : , : , :
35instantiation45, 264, 127, 86, 291, 46  ⊢  
  : , : , :
36instantiation47, 48  ⊢  
  :
37instantiation49, 272, 50  ⊢  
  : , :
38instantiation191, 192, 290, 319, 193, 52, 84, 65, 51  ⊢  
  : , : , : , : , : , :
39instantiation191, 290, 192, 52, 193, 84, 65  ⊢  
  : , : , : , : , : , :
40instantiation136, 53, 54, 55  ⊢  
  : , : , : , :
41instantiation56, 65, 169  ⊢  
  : , :
42instantiation121, 295  ⊢  
  :
43instantiation270  ⊢  
  : , :
44instantiation317, 279, 57  ⊢  
  : , : , :
45conjecture  ⊢  
 proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
46instantiation187, 179, 217, 178, 58  ⊢  
  : , : , :
47conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
48instantiation59, 290, 99  ⊢  
  : , :
49conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_basic
50instantiation219  ⊢  
  :
51instantiation317, 279, 60  ⊢  
  : , : , :
52instantiation270  ⊢  
  : , :
53instantiation106, 319, 84, 65  ⊢  
  : , : , : , : , : , : , :
54instantiation107, 192, 290, 193, 61, 63, 84, 65, 62*  ⊢  
  : , : , : , : , : , :
55instantiation107, 319, 290, 192, 63, 193, 64, 65, 66*  ⊢  
  : , : , : , : , : , :
56conjecture  ⊢  
 proveit.numbers.addition.commutation
57instantiation98, 264, 67  ⊢  
  : , :
58instantiation68, 264, 240, 119  ⊢  
  : , :
59conjecture  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
60instantiation177, 92, 90  ⊢  
  : , :
61instantiation270  ⊢  
  : , :
62instantiation69, 70, 71*  ⊢  
  : , :
63instantiation270  ⊢  
  : , :
64instantiation72, 251, 73  ⊢  
  : , :
65instantiation164, 272  ⊢  
  :
66instantiation74, 272, 251, 142  ⊢  
  : , : , :
67instantiation103, 75, 76  ⊢  
  :
68conjecture  ⊢  
 proveit.numbers.negation.negated_weak_bound
69theorem  ⊢  
 proveit.logic.equality.equals_reversal
70instantiation77, 192, 290, 319, 193, 78, 272, 84, 79*  ⊢  
  : , : , : , : , : , :
71instantiation245, 80, 81  ⊢  
  : , : , :
72conjecture  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
73instantiation317, 279, 82  ⊢  
  : , : , :
74conjecture  ⊢  
 proveit.numbers.addition.subtraction.negated_add
75instantiation110, 111, 83  ⊢  
  : , :
76instantiation113, 120  ⊢  
  : , :
77conjecture  ⊢  
 proveit.numbers.multiplication.distribute_through_sum
78instantiation270  ⊢  
  : , :
79instantiation238, 84  ⊢  
  :
80instantiation224, 142  ⊢  
  : , : , :
81instantiation85, 251, 311, 86, 87, 88*, 89*  ⊢  
  : , : , :
82instantiation177, 90, 179  ⊢  
  : , :
83instantiation317, 117, 91  ⊢  
  : , : , :
84instantiation317, 279, 92  ⊢  
  : , : , :
85conjecture  ⊢  
 proveit.numbers.exponentiation.product_of_real_powers
86instantiation317, 313, 93  ⊢  
  : , : , :
87instantiation94, 307  ⊢  
  :
88instantiation95, 251  ⊢  
  :
89instantiation245, 96, 97  ⊢  
  : , : , :
90instantiation239, 311  ⊢  
  :
91instantiation121, 256  ⊢  
  :
92instantiation98, 264, 99  ⊢  
  : , :
93instantiation317, 315, 104  ⊢  
  : , : , :
94conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
95conjecture  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
96instantiation191, 319, 290, 192, 100, 193, 272, 169, 150  ⊢  
  : , : , : , : , : , :
97instantiation245, 101, 102  ⊢  
  : , : , :
98conjecture  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
99instantiation103, 104, 105  ⊢  
  :
100instantiation270  ⊢  
  : , :
101instantiation106, 319, 192, 193, 272, 169, 150  ⊢  
  : , : , : , : , : , : , :
102instantiation107, 192, 290, 319, 193, 108, 272, 150, 169, 109*  ⊢  
  : , : , : , : , : , :
103conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonneg_int_is_natural
104instantiation110, 111, 112  ⊢  
  : , :
105instantiation113, 114  ⊢  
  : , :
106conjecture  ⊢  
 proveit.numbers.addition.leftward_commutation
107conjecture  ⊢  
 proveit.numbers.addition.association
108instantiation270  ⊢  
  : , :
109instantiation115, 272, 251, 142  ⊢  
  : , : , :
110conjecture  ⊢  
 proveit.numbers.addition.add_int_closure_bin
111instantiation317, 116, 200  ⊢  
  : , : , :
112instantiation317, 117, 118  ⊢  
  : , : , :
113conjecture  ⊢  
 proveit.numbers.addition.subtraction.nonneg_difference
114instantiation143, 119, 120  ⊢  
  : , : , :
115conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add_reversed
116conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
117conjecture  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
118instantiation121, 307  ⊢  
  :
119axiom  ⊢  
 proveit.physics.quantum.QPE._n_ge_two
120instantiation158, 162, 264, 122, 123, 124*, 125*  ⊢  
  : , : , :
121conjecture  ⊢  
 proveit.numbers.negation.int_neg_closure
122instantiation177, 127, 264  ⊢  
  : , :
123instantiation126, 264, 127, 128, 234  ⊢  
  : , : , :
124instantiation245, 129, 130  ⊢  
  : , : , :
125instantiation245, 131, 132  ⊢  
  : , : , :
126conjecture  ⊢  
 proveit.numbers.ordering.less_eq_add_right
127instantiation177, 179, 217  ⊢  
  : , :
128instantiation143, 133, 134  ⊢  
  : , : , :
129instantiation191, 319, 290, 192, 149, 193, 251, 197, 150  ⊢  
  : , : , : , : , : , :
130instantiation196, 251, 197, 167  ⊢  
  : , : , :
131instantiation224, 135  ⊢  
  : , : , :
132instantiation136, 137, 138, 139  ⊢  
  : , : , : , :
133instantiation140, 316, 156, 141, 142*  ⊢  
  : , :
134instantiation143, 144, 145  ⊢  
  : , : , :
135instantiation191, 192, 290, 319, 193, 166, 169, 195, 251  ⊢  
  : , : , : , : , : , :
136conjecture  ⊢  
 proveit.logic.equality.four_chain_transitivity
137instantiation191, 192, 147, 319, 193, 148, 169, 195, 251, 146  ⊢  
  : , : , : , : , : , :
138instantiation191, 147, 290, 192, 148, 149, 193, 169, 195, 251, 197, 150  ⊢  
  : , : , : , : , : , :
139instantiation245, 151, 152  ⊢  
  : , : , :
140conjecture  ⊢  
 proveit.numbers.rounding.ceil_of_real_above_int
141instantiation153, 299, 173, 154  ⊢  
  : , :
142conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
143conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
144instantiation155, 156, 268, 157  ⊢  
  : , :
145instantiation158, 217, 159, 179, 160, 161*  ⊢  
  : , : , :
146instantiation317, 279, 162  ⊢  
  : , : , :
147conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat3
148instantiation163  ⊢  
  : , : , :
149instantiation270  ⊢  
  : , :
150instantiation164, 251  ⊢  
  :
151instantiation165, 290, 319, 192, 166, 193, 169, 195, 251, 197, 167  ⊢  
  : , : , : , : , : , : , : , :
152instantiation168, 197, 169, 199  ⊢  
  : , : , :
153conjecture  ⊢  
 proveit.numbers.logarithms.log_base_large_a_greater_one
154instantiation170, 291, 171  ⊢  
  : , :
155conjecture  ⊢  
 proveit.numbers.rounding.ceil_increasing_less_eq
156instantiation274, 299, 173, 276  ⊢  
  : , :
157instantiation172, 299, 173, 275, 174, 291  ⊢  
  : , : , :
158conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
159instantiation177, 240, 218  ⊢  
  : , :
160axiom  ⊢  
 proveit.physics.quantum.QPE._t_req
161instantiation245, 175, 176  ⊢  
  : , : , :
162instantiation177, 240, 178  ⊢  
  : , :
163conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
164conjecture  ⊢  
 proveit.numbers.negation.complex_closure
165conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_general
166instantiation270  ⊢  
  : , :
167instantiation219  ⊢  
  :
168conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_32
169instantiation317, 279, 179  ⊢  
  : , : , :
170theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
171instantiation180, 264, 181, 182, 183, 184*, 185*  ⊢  
  : , : , :
172conjecture  ⊢  
 proveit.numbers.logarithms.log_increasing_less_eq
173instantiation317, 301, 186  ⊢  
  : , : , :
174instantiation187, 264, 258, 188, 189, 190*  ⊢  
  : , : , :
175instantiation191, 192, 290, 319, 193, 194, 197, 198, 195  ⊢  
  : , : , : , : , : , :
176instantiation196, 197, 198, 199  ⊢  
  : , : , :
177conjecture  ⊢  
 proveit.numbers.addition.add_real_closure_bin
178instantiation239, 264  ⊢  
  :
179instantiation254, 255, 200  ⊢  
  : , : , :
180conjecture  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
181instantiation201, 258, 310  ⊢  
  : , :
182instantiation317, 313, 202  ⊢  
  : , : , :
183instantiation203, 258, 310, 311, 204, 205  ⊢  
  : , : , :
184instantiation245, 206, 207  ⊢  
  : , : , :
185instantiation245, 208, 209  ⊢  
  : , : , :
186instantiation285, 210, 302  ⊢  
  : , :
187conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_right_term_bound
188instantiation317, 211, 282  ⊢  
  : , : , :
189instantiation212, 213, 297, 299, 214  ⊢  
  : , : , :
190instantiation226, 280, 316, 227*, 215*, 216*  ⊢  
  : , : , : , :
191conjecture  ⊢  
 proveit.numbers.addition.disassociation
192axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
193conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
194instantiation270  ⊢  
  : , :
195instantiation317, 279, 217  ⊢  
  : , : , :
196conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_13
197instantiation317, 279, 240  ⊢  
  : , : , :
198instantiation317, 279, 218  ⊢  
  : , : , :
199instantiation219  ⊢  
  :
200axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
201conjecture  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
202instantiation220, 269, 314  ⊢  
  : , :
203conjecture  ⊢  
 proveit.numbers.multiplication.strong_bound_via_right_factor_bound
204conjecture  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
205instantiation221, 278  ⊢  
  :
206instantiation224, 222  ⊢  
  : , : , :
207instantiation223, 251  ⊢  
  :
208instantiation224, 225  ⊢  
  : , : , :
209instantiation226, 316, 280, 227*, 228*, 235*  ⊢  
  : , : , : , :
210instantiation317, 306, 229  ⊢  
  : , : , :
211conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
212conjecture  ⊢  
 proveit.numbers.division.weak_div_from_denom_bound__all_pos
213instantiation317, 230, 231  ⊢  
  : , : , :
214instantiation232, 264, 304, 311, 233, 234, 235*  ⊢  
  : , : , :
215instantiation245, 236, 237  ⊢  
  : , : , :
216instantiation238, 251  ⊢  
  :
217instantiation239, 240  ⊢  
  :
218instantiation317, 313, 241  ⊢  
  : , : , :
219axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
220conjecture  ⊢  
 proveit.numbers.multiplication.mult_rational_closure_bin
221conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
222instantiation242, 243  ⊢  
  :
223conjecture  ⊢  
 proveit.numbers.addition.elim_zero_left
224axiom  ⊢  
 proveit.logic.equality.substitution
225instantiation271, 243  ⊢  
  :
226conjecture  ⊢  
 proveit.numbers.addition.rational_pair_addition
227instantiation244, 251  ⊢  
  :
228instantiation245, 246, 247  ⊢  
  : , : , :
229conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat5
230conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
231instantiation317, 248, 319  ⊢  
  : , : , :
232conjecture  ⊢  
 proveit.numbers.multiplication.weak_bound_via_right_factor_bound
233instantiation249, 310, 311, 312  ⊢  
  : , : , :
234instantiation250, 290  ⊢  
  :
235instantiation271, 251  ⊢  
  :
236instantiation259, 290, 252, 253, 263, 262  ⊢  
  : , : , : , :
237conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_4_1
238conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_left
239conjecture  ⊢  
 proveit.numbers.negation.real_closure
240instantiation254, 255, 256  ⊢