Proof of proveit.physics.quantum.QPE._failure_upper_bound_lemma theorem

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, e, l, m, defaults
from proveit.logic import InSet
from proveit.numbers import Add, Neg, frac, one, four, NaturalPos, IntegerNeg
# import common expressions
from proveit.physics.quantum.QPE import _neg_domain, _pos_domain, ModAdd
# import theorems
from proveit.physics.quantum.QPE import (
    _b_floor, _alpha_sqrd_upper_bound, _alpha_are_complex, 
    _t_in_natural_pos, _two_pow_t_is_nat_pos, _two_pow_t_minus_one_is_nat_pos,
    _fail_sum, _delta_b_is_real, _best_floor_is_int,
    _scaled_delta_b_not_eq_nonzeroInt)

%proving _failure_upper_bound_lemma

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_failure_upper_bound_lemma:
(see dependencies)

defaults.assumptions = _failure_upper_bound_lemma.conditions

defaults.assumptions:

defaults.preserved_exprs = {Neg(Add(e, one))} # don't simplify to -e - 1

defaults.preserved_exprs:

Instantiate some needed theorems of this package

pos_assumptions = (InSet(l, _pos_domain),)+tuple(defaults.assumptions)

pos_assumptions:

neg_assumptions = (InSet(l, _neg_domain),)+tuple(defaults.assumptions)

neg_assumptions:

_alpha_sqrd_upper_bound.instantiate(assumptions=pos_assumptions).generalize(l, domain=_pos_domain)

 ⊢  

_alpha_sqrd_upper_bound.instantiate(assumptions=neg_assumptions).generalize(l, domain=_neg_domain)

 ⊢  

_best_floor_is_int

 ⊢  

_delta_b_is_real

 ⊢  

_delta_b_is_real.instantiate({b:_b_floor})

 ⊢  

_scaled_delta_b_not_eq_nonzeroInt

 ⊢  

_scaled_delta_b_not_eq_nonzeroInt.instantiate({b:_b_floor}, assumptions=pos_assumptions)

,  ⊢  

_scaled_delta_b_not_eq_nonzeroInt.instantiate({b:_b_floor}, assumptions=neg_assumptions)

,  ⊢  

_alpha_are_complex

 ⊢  

_alpha_are_complex.instantiate({m:ModAdd(_b_floor, l)}, assumptions=pos_assumptions)

,  ⊢  

_alpha_are_complex.instantiate({m:ModAdd(_b_floor, l)}, assumptions=neg_assumptions)

,  ⊢  

fail_sum_inst = _fail_sum.instantiate()

fail_sum_inst:  ⊢  

Upper bound each of the summations in fail_sum_inst via _alpha_sqrd_upper_bound

first_sum = fail_sum_inst.rhs.terms[0]

first_sum:

second_sum = fail_sum_inst.rhs.terms[1]

second_sum:

_alpha_sqrd_upper_bound

 ⊢  

first_sum_bound = first_sum.deduce_bound(_alpha_sqrd_upper_bound)

first_sum_bound:  ⊢  

second_sum_bound = second_sum.deduce_bound(_alpha_sqrd_upper_bound)

second_sum_bound:  ⊢  

Bound the sum of summations by the bound of the sum and simplify

bound_rhs = fail_sum_inst.rhs.deduce_bound([first_sum_bound, second_sum_bound])

bound_rhs:  ⊢  

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

not_yet_factored = fail_sum_inst.apply_transitivity(bound_rhs)

not_yet_factored:  ⊢  

not_yet_factored.inner_expr().rhs.factor(frac(one, four), auto_simplify=False)

 ⊢  

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4	⊢
	: , : , :
2	theorem		⊢
	proveit.logic.equality.sub_right_side_into
3	instantiation	197, 5, 6	⊢
	: , : , :
4	instantiation	192, 7, 8, 9	⊢
	: , : , : , :
5	instantiation	10, 11, 12	⊢
	: , : , :
6	instantiation	13, 288	⊢
	:
7	instantiation	213, 14	⊢
	: , : , :
8	instantiation	213, 15	⊢
	: , : , :
9	instantiation	211, 16	⊢
	: , :
10	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
11	instantiation	137, 21, 17, 20, 18	⊢
	: , : , :
12	instantiation	19, 20, 21, 22, 23	⊢
	: , : , :
13	conjecture		⊢
	proveit.physics.quantum.QPE._fail_sum
14	instantiation	157, 24, 25	⊢
	: , : , :
15	instantiation	157, 26, 27	⊢
	: , : , :
16	instantiation	28, 289, 299, 207, 29, 208, 64, 30, 31	⊢
	: , : , : , : , : , :
17	modus ponens	32, 33	⊢
18	modus ponens	34, 35	⊢
19	conjecture		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
20	modus ponens	36, 37	⊢
21	modus ponens	38, 39	⊢
22	modus ponens	40, 41	⊢
23	modus ponens	42, 43	⊢
24	instantiation	213, 44	⊢
	: , : , :
25	instantiation	211, 45	⊢
	: , :
26	instantiation	213, 46	⊢
	: , : , :
27	instantiation	211, 47	⊢
	: , :
28	conjecture		⊢
	proveit.numbers.multiplication.distribute_through_sum
29	instantiation	103	⊢
	: , :
30	modus ponens	48, 77	⊢
31	modus ponens	49, 81	⊢
32	instantiation	54	⊢
	: , : , :
33	generalization	50	⊢
34	instantiation	56	⊢
	: , : , :
35	generalization	51	⊢
36	instantiation	54	⊢
	: , : , :
37	generalization	52	⊢
38	instantiation	54	⊢
	: , : , :
39	generalization	53	⊢
40	instantiation	54	⊢
	: , : , :
41	generalization	55	⊢
42	instantiation	56	⊢
	: , : , :
43	generalization	57	⊢
44	modus ponens	58, 59	⊢
45	instantiation	60, 208, 64	⊢
	: , :
46	modus ponens	61, 62	⊢
47	instantiation	63, 208, 64	⊢
	: , :
48	instantiation	65	⊢
	: , : , :
49	instantiation	65	⊢
	: , : , :
50	instantiation	133, 66, 299	,  ⊢
	: , :
51	instantiation	73, 67, 186	,  ⊢
	:
52	instantiation	123, 261, 68, 69	,  ⊢
	: , :
53	instantiation	133, 70, 299	,  ⊢
	: , :
54	conjecture		⊢
	proveit.numbers.summation.summation_real_closure
55	instantiation	123, 261, 71, 72	,  ⊢
	: , :
56	conjecture		⊢
	proveit.numbers.summation.weak_summation_from_summands_bound
57	instantiation	73, 74, 191	,  ⊢
	:
58	instantiation	78, 267	⊢
	: , : , : , : , : , : , :
59	generalization	75	⊢
60	modus ponens	76, 77	⊢
61	instantiation	78, 267	⊢
	: , : , : , : , : , : , :
62	generalization	79	⊢
63	modus ponens	80, 81	⊢
64	instantiation	297, 260, 82	⊢
	: , : , :
65	conjecture		⊢
	proveit.numbers.summation.summation_complex_closure
66	instantiation	297, 85, 83	,  ⊢
	: , : , :
67	instantiation	89, 235, 291, 200, 84	,  ⊢
	: , : , :
68	instantiation	203, 96, 119	,  ⊢
	: , :
69	instantiation	87, 299, 88, 109, 131	,  ⊢
	: , :
70	instantiation	297, 85, 86	,  ⊢
	: , : , :
71	instantiation	203, 96, 124	,  ⊢
	: , :
72	instantiation	87, 299, 88, 109, 135	,  ⊢
	: , :
73	conjecture		⊢
	proveit.physics.quantum.QPE._alpha_sqrd_upper_bound
74	instantiation	89, 235, 291, 223, 90	,  ⊢
	: , : , :
75	instantiation	211, 91	,  ⊢
	: , :
76	instantiation	94, 289, 267, 207	⊢
	: , : , : , : , : , :
77	generalization	92	⊢
78	conjecture		⊢
	proveit.core_expr_types.lambda_maps.general_lambda_substitution
79	instantiation	211, 93	,  ⊢
	: , :
80	instantiation	94, 289, 267, 207	⊢
	: , : , : , : , : , :
81	generalization	95	⊢
82	instantiation	123, 261, 96, 97	⊢
	: , :
83	instantiation	101, 98	,  ⊢
	:
84	instantiation	104, 99, 100	,  ⊢
	: , :
85	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.real_nonneg_within_real
86	instantiation	101, 102	,  ⊢
	:
87	conjecture		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
88	instantiation	103	⊢
	: , :
89	conjecture		⊢
	proveit.numbers.number_sets.integers.in_interval
90	instantiation	104, 105, 106	,  ⊢
	: , :
91	instantiation	108, 245, 109, 131, 110*	,  ⊢
	: , : , : , :
92	instantiation	297, 260, 107	,  ⊢
	: , : , :
93	instantiation	108, 245, 109, 135, 110*	,  ⊢
	: , : , : , :
94	conjecture		⊢
	proveit.numbers.multiplication.distribute_through_summation
95	instantiation	297, 260, 111	,  ⊢
	: , : , :
96	instantiation	297, 270, 112	⊢
	: , : , :
97	instantiation	248, 152	⊢
	:
98	instantiation	115, 113	,  ⊢
	:
99	instantiation	285, 235, 236, 237	,  ⊢
	: , : , :
100	instantiation	117, 114	,  ⊢
	: , :
101	conjecture		⊢
	proveit.numbers.absolute_value.abs_complex_closure
102	instantiation	115, 116	,  ⊢
	:
103	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
104	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
105	instantiation	117, 118	,  ⊢
	: , :
106	instantiation	234, 255, 291, 256	,  ⊢
	: , : , :
107	instantiation	123, 261, 119, 120	,  ⊢
	: , :
108	conjecture		⊢
	proveit.numbers.division.prod_of_fracs
109	instantiation	297, 249, 121	⊢
	: , : , :
110	instantiation	122, 245	⊢
	:
111	instantiation	123, 261, 124, 125	,  ⊢
	: , :
112	instantiation	297, 277, 126	⊢
	: , : , :
113	instantiation	129, 222, 200	,  ⊢
	: , :
114	instantiation	127, 202, 128	,  ⊢
	: , : , :
115	conjecture		⊢
	proveit.physics.quantum.QPE._alpha_are_complex
116	instantiation	129, 222, 223	,  ⊢
	: , :
117	conjecture		⊢
	proveit.numbers.ordering.relax_less
118	instantiation	217, 130, 224	,  ⊢
	: , : , :
119	instantiation	133, 163, 299	,  ⊢
	: , :
120	instantiation	134, 131	,  ⊢
	:
121	instantiation	297, 263, 132	⊢
	: , : , :
122	conjecture		⊢
	proveit.numbers.multiplication.elim_one_left
123	conjecture		⊢
	proveit.numbers.division.div_real_closure
124	instantiation	133, 165, 299	,  ⊢
	: , :
125	instantiation	134, 135	,  ⊢
	:
126	instantiation	297, 298, 136	⊢
	: , : , :
127	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
128	instantiation	253, 294	⊢
	:
129	conjecture		⊢
	proveit.physics.quantum.QPE._mod_add_closure
130	instantiation	137, 156, 261, 138, 139, 140*, 141*	⊢
	: , : , :
131	instantiation	144, 142, 229	,  ⊢
	: , :
132	instantiation	297, 272, 143	⊢
	: , : , :
133	conjecture		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
134	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_if_in_complex_nonzero
135	instantiation	144, 145, 229	,  ⊢
	: , :
136	conjecture		⊢
	proveit.numbers.numerals.decimals.nat4
137	conjecture		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
138	instantiation	257, 258, 294	⊢
	: , : , :
139	instantiation	146, 294	⊢
	:
140	instantiation	225, 245, 147	⊢
	: , :
141	instantiation	157, 148, 149	⊢
	: , : , :
142	instantiation	153, 150, 151	,  ⊢
	:
143	instantiation	297, 278, 152	⊢
	: , : , :
144	conjecture		⊢
	proveit.numbers.exponentiation.exp_complex_nonzero_closure
145	instantiation	153, 154, 155	,  ⊢
	:
146	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
147	instantiation	297, 260, 156	⊢
	: , : , :
148	instantiation	157, 158, 159	⊢
	: , : , :
149	instantiation	160, 161, 162	⊢
	: , :
150	instantiation	297, 260, 163	,  ⊢
	: , : , :
151	instantiation	166, 164	,  ⊢
	: , :
152	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat4
153	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
154	instantiation	297, 260, 165	,  ⊢
	: , : , :
155	instantiation	166, 167	,  ⊢
	: , :
156	instantiation	297, 270, 168	⊢
	: , : , :
157	axiom		⊢
	proveit.logic.equality.equals_transitivity
158	instantiation	213, 181	⊢
	: , : , :
159	instantiation	213, 169	⊢
	: , : , :
160	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
161	instantiation	170, 171, 172	⊢
	: , :
162	instantiation	173	⊢
	:
163	instantiation	176, 174, 178	,  ⊢
	: , :
164	instantiation	179, 175	,  ⊢
	: , :
165	instantiation	176, 177, 178	,  ⊢
	: , :
166	conjecture		⊢
	proveit.numbers.addition.subtraction.nonzero_difference_if_different
167	instantiation	179, 180	,  ⊢
	: , :
168	instantiation	297, 277, 251	⊢
	: , : , :
169	instantiation	213, 181	⊢
	: , : , :
170	conjecture		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
171	instantiation	182, 245, 183, 184	⊢
	: , :
172	instantiation	297, 260, 204	⊢
	: , : , :
173	axiom		⊢
	proveit.logic.equality.equals_reflexivity
174	instantiation	297, 270, 185	,  ⊢
	: , : , :
175	instantiation	189, 190, 200, 186	,  ⊢
	: , :
176	conjecture		⊢
	proveit.numbers.addition.add_real_closure_bin
177	instantiation	297, 270, 187	,  ⊢
	: , : , :
178	instantiation	247, 188	⊢
	:
179	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
180	instantiation	189, 190, 223, 191	,  ⊢
	: , :
181	instantiation	192, 193, 194, 195	⊢
	: , : , : , :
182	conjecture		⊢
	proveit.numbers.division.div_complex_closure
183	instantiation	196, 229, 245	⊢
	: , :
184	instantiation	197, 231, 198	⊢
	: , : , :
185	instantiation	297, 277, 200	,  ⊢
	: , : , :
186	instantiation	199, 200, 201, 202	,  ⊢
	: , :
187	instantiation	297, 277, 223	,  ⊢
	: , : , :
188	instantiation	203, 204, 205	⊢
	: , :
189	conjecture		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_not_eq_nonzeroInt
190	instantiation	206, 207, 289, 208	⊢
	: , : , : , : , :
191	instantiation	248, 209	,  ⊢
	:
192	conjecture		⊢
	proveit.logic.equality.four_chain_transitivity
193	instantiation	213, 210	⊢
	: , : , :
194	instantiation	211, 212	⊢
	: , :
195	instantiation	213, 214	⊢
	: , : , :
196	conjecture		⊢
	proveit.numbers.exponentiation.exp_complex_closure
197	theorem		⊢
	proveit.logic.equality.sub_left_side_into
198	instantiation	215, 229	⊢
	:
199	conjecture		⊢
	proveit.numbers.ordering.less_is_not_eq_int
200	instantiation	297, 216, 237	,  ⊢
	: , : , :
201	conjecture		⊢
	proveit.numbers.number_sets.integers.zero_is_int
202	instantiation	217, 218, 219	,  ⊢
	: , : , :
203	conjecture		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
204	instantiation	257, 258, 220	⊢
	: , : , :
205	instantiation	221, 222	⊢
	:
206	conjecture		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
207	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
208	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
209	instantiation	274, 223, 224	,  ⊢
	:
210	instantiation	225, 226, 227	⊢
	: , :
211	theorem		⊢
	proveit.logic.equality.equals_reversal
212	instantiation	228, 229, 230, 243, 231	⊢
	: , : , :
213	axiom		⊢
	proveit.logic.equality.substitution
214	instantiation	232, 233, 267	⊢
	: , :
215	conjecture		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
216	instantiation	284, 235, 236	⊢
	: , :
217	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
218	instantiation	234, 235, 236, 237	,  ⊢
	: , : , :
219	instantiation	238, 239	⊢
	:
220	conjecture		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
221	conjecture		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
222	conjecture		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
223	instantiation	297, 240, 256	,  ⊢
	: , : , :
224	instantiation	281, 241, 242	,  ⊢
	: , : , :
225	conjecture		⊢
	proveit.numbers.addition.commutation
226	instantiation	297, 260, 243	⊢
	: , : , :
227	instantiation	244, 245	⊢
	:
228	conjecture		⊢
	proveit.numbers.exponentiation.product_of_real_powers
229	instantiation	297, 260, 246	⊢
	: , : , :
230	instantiation	247, 261	⊢
	:
231	instantiation	248, 279	⊢
	:
232	conjecture		⊢
	proveit.numbers.exponentiation.neg_power_as_div
233	instantiation	297, 249, 250	⊢
	: , : , :
234	conjecture		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
235	instantiation	290, 251, 286	⊢
	: , :
236	instantiation	295, 255	⊢
	:
237	assumption		⊢
238	conjecture		⊢
	proveit.numbers.number_sets.integers.negative_if_in_neg_int
239	instantiation	252, 254	⊢
	:
240	instantiation	284, 255, 291	⊢
	: , :
241	instantiation	253, 254	⊢
	:
242	instantiation	285, 255, 291, 256	,  ⊢
	: , : , :
243	instantiation	257, 258, 259	⊢
	: , : , :
244	conjecture		⊢
	proveit.numbers.negation.complex_closure
245	instantiation	297, 260, 261	⊢
	: , : , :
246	instantiation	297, 270, 262	⊢
	: , : , :
247	conjecture		⊢
	proveit.numbers.negation.real_closure
248	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
249	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
250	instantiation	297, 263, 264	⊢
	: , : , :
251	instantiation	295, 291	⊢
	:
252	conjecture		⊢
	proveit.numbers.negation.int_neg_closure
253	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
254	instantiation	265, 266, 267	⊢
	: , :
255	instantiation	290, 275, 286	⊢
	: , :
256	assumption		⊢
257	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
258	instantiation	268, 269	⊢
	: , :
259	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
260	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
261	instantiation	297, 270, 271	⊢
	: , : , :
262	instantiation	297, 277, 296	⊢
	: , : , :
263	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
264	instantiation	297, 272, 273	⊢
	: , : , :
265	conjecture		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
266	instantiation	274, 275, 276	⊢
	:
267	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
268	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
269	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
270	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
271	instantiation	297, 277, 286	⊢
	: , : , :
272	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
273	instantiation	297, 278, 279	⊢
	: , : , :
274	conjecture		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
275	instantiation	297, 280, 288	⊢
	: , : , :
276	instantiation	281, 282, 283	⊢
	: , : , :
277	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
278	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
279	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
280	instantiation	284, 286, 287	⊢
	: , :
281	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
282	conjecture		⊢
	proveit.numbers.numerals.decimals.less_0_1
283	instantiation	285, 286, 287, 288	⊢
	: , : , :
284	conjecture		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
285	conjecture		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
286	instantiation	297, 298, 289	⊢
	: , : , :
287	instantiation	290, 291, 292	⊢
	: , :
288	assumption		⊢
289	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
290	conjecture		⊢
	proveit.numbers.addition.add_int_closure_bin
291	instantiation	297, 293, 294	⊢
	: , : , :
292	instantiation	295, 296	⊢
	:
293	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
294	conjecture		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
295	conjecture		⊢
	proveit.numbers.negation.int_closure
296	instantiation	297, 298, 299	⊢
	: , : , :
297	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
298	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
299	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements