Proof of proveit.physics.quantum.QPE._best_guarantee theorem¶

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

from proveit import defaults
from proveit import b, m
from proveit.logic import Or, Equals, InSet
from proveit.numbers import zero, one, Integer, Neg, Abs, Mod, sqrd
from proveit.numbers.number_sets.real_numbers import pi_between_3_and_4
from proveit.physics.quantum.QPE import (
_best_guarantee_delta_nonzero, _alpha_ideal_case,
_phase_is_real, _phase_in_interval,
_b_round, _best_round_def, _best_round_is_int, _delta_b_round, _delta_b_def,
_two_pow_t, _t_in_natural_pos, _two_pow_t_is_nat_pos)

In [2]:
%proving _best_guarantee

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

In [4]:
four_over_pi_sqrd = _best_guarantee_delta_nonzero.consequent.rhs

four_over_pi_sqrd:
In [5]:
_alpha_ideal_case


Show that when $\delta_{b_r}=0$ then $(2^t \varphi) \in \{0 .. 2^t - 1\}$¶

In [6]:
defaults.assumptions = [Equals(_delta_b_round, zero)]

defaults.assumptions:
In [7]:
_delta_b_def

In [8]:
delta_b_definition = _delta_b_def.instantiate({b:_b_round})

delta_b_definition:
In [9]:
phase_rel_01 = _delta_b_def.instantiate({b:_b_round}).inner_expr().lhs.substitute(zero)

phase_rel_01:
In [10]:
phase_rel_02 = phase_rel_01.right_add_both_sides(phase_rel_01.rhs.operands[1].operand).derive_reversed()

phase_rel_02:
In [11]:
phase_rel_03 = phase_rel_02.left_mult_both_sides(_two_pow_t)

phase_rel_03:
In [12]:
_best_round_def

In [13]:
InSet(phase_rel_03.lhs, Integer).prove()

In [14]:
_phase_in_interval

In [15]:
phase_lower_bound = _phase_in_interval.derive_element_lower_bound()

phase_lower_bound:
In [16]:
phase_lower_bound.left_mult_both_sides(_two_pow_t)

In [17]:
phase_upper_bound = _phase_in_interval.derive_element_upper_bound()

phase_upper_bound:
In [18]:
scaled_phase_upper_bound = phase_upper_bound.left_mult_both_sides(_two_pow_t)

scaled_phase_upper_bound:
In [19]:
scaled_phase_upper_bound.add_right(Neg(one), strong=False)

In [20]:
ideal_alpha_01 = _alpha_ideal_case.derive_consequent()

ideal_alpha_01:

Replace $2^t \varphi$ with $b_r~\textrm{mod}~2^t$ assuming $\delta_{b_r} = 0$¶

In [21]:
ideal_alpha_02 = phase_rel_03.sub_right_side_into(ideal_alpha_01)

ideal_alpha_02:
In [22]:
_alpha_ideal_case.antecedent

In [23]:
InSet(_b_round, _alpha_ideal_case.antecedent.domain).prove()

In [24]:
b_r_mod__eq__br = Mod(_b_round, _two_pow_t).simplification()

b_r_mod__eq__br:
In [25]:
ideal_alpha_03 = b_r_mod__eq__br.sub_left_side_into(ideal_alpha_02)

ideal_alpha_03:

Now we can prove that $|\alpha_{b_r~\textrm{mod}~2^t}|^2 > 4/\pi^2$ whether or not $\delta_{b_r} = 0$¶

In [26]:
defaults.preserved_exprs={Abs(ideal_alpha_03.lhs), sqrd(Abs(ideal_alpha_03.lhs))}
ideal_alpha_03.abs_both_sides().square_both_sides()

In [27]:
pi_between_3_and_4

In [28]:
four_over_pi_sqrd_bound = four_over_pi_sqrd.deduce_bound(pi_between_3_and_4.operands[0].reversed())

four_over_pi_sqrd_bound:
In [29]:
from proveit.numbers import Less, num
Less(num(4), num(9)).prove().divide_both_sides(num(9))

In [30]:
eq_or_not = Or(defaults.assumptions[0], _best_guarantee_delta_nonzero.antecedent)

eq_or_not:
In [31]:
defaults.assumptions = []
alpha_sqrd_bound = eq_or_not.derive_via_dilemma(_best_guarantee_delta_nonzero.consequent)

alpha_sqrd_bound:
In [32]:
_best_round_def.sub_right_side_into(alpha_sqrd_bound)

_best_guarantee has been proven.  Now simply execute "%qed".

In [33]:
%qed

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

Out[33]:
step typerequirementsstatement
0instantiation1, 2, 3
: , : , :
1reference190
2instantiation4, 15, 5, 6, 7, 8
: , : , :
3axiom
proveit.physics.quantum.QPE._best_round_def
4theorem
proveit.logic.booleans.disjunction.singular_constructive_dilemma
5instantiation9
: , :
6instantiation10, 11, 12
: , :
7deduction13
8conjecture
proveit.physics.quantum.QPE._best_guarantee_delta_nonzero
9conjecture
proveit.logic.equality.not_equals_is_bool
10theorem
proveit.logic.equality.rhs_via_equality
11instantiation14, 15
:
12instantiation228, 16
: , : , :
13instantiation44, 17, 18
: , : , :
14conjecture
proveit.logic.booleans.unfold_is_bool
15instantiation19
: , :
16instantiation162, 20
: , :
17instantiation21, 22, 23, 24, 61
: , : , :
18instantiation146, 25, 26
: , : , :
19axiom
proveit.logic.equality.equality_in_bool
20instantiation27
: , :
21conjecture
proveit.numbers.division.strong_div_from_denom_bound__all_pos
22instantiation254, 29, 28
: , : , :
23instantiation254, 29, 30
: , : , :
24instantiation31, 32, 33
:
25instantiation34, 66, 94, 35, 60, 36*
: , : , :
26instantiation37, 73, 38, 222, 39, 40*
: , : , :
27axiom
proveit.logic.equality.not_equals_def
28instantiation254, 42, 41
: , : , :
29conjecture
proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
30instantiation254, 42, 71
: , : , :
31conjecture
proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
32instantiation43, 74, 195
: , :
33instantiation44, 45
: , : , :
34conjecture
proveit.numbers.division.strong_div_from_numer_bound__pos_denom
35instantiation46, 94, 158, 47, 48, 49*, 50*
: , : , :
36instantiation51, 52, 53
:
37conjecture
proveit.numbers.exponentiation.exp_eq_real
38instantiation254, 54, 55
: , : , :
39instantiation56, 68, 207, 84, 57*
: , :
40instantiation58, 59
:
41conjecture
proveit.numbers.numerals.decimals.posnat4
42conjecture
proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
43conjecture
proveit.numbers.exponentiation.exp_real_closure_nat_power
44axiom
proveit.numbers.ordering.transitivity_less_less
45instantiation131, 60, 61
: , :
46conjecture
47instantiation254, 233, 62
: , : , :
48instantiation160, 63
:
49instantiation190, 64, 65
: , : , :
50conjecture
51conjecture
proveit.numbers.division.frac_cancel_complete
52instantiation254, 244, 66
: , : , :
53instantiation251, 71
:
54conjecture
proveit.numbers.number_sets.real_numbers.real_nonneg_within_real
55instantiation67, 68
:
56conjecture
proveit.numbers.absolute_value.abs_eq
57instantiation69, 70
:
58conjecture
proveit.numbers.exponentiation.exponentiated_one
59instantiation254, 244, 73
: , : , :
60instantiation160, 71
:
61instantiation72, 73, 114, 74, 75, 76, 77*
: , : , :
62instantiation254, 249, 78
: , : , :
63conjecture
proveit.numbers.numerals.decimals.posnat5
64instantiation79, 81
:
65instantiation80, 81, 82
: , :
66instantiation254, 233, 83
: , : , :
67conjecture
proveit.numbers.absolute_value.abs_complex_closure
68instantiation146, 207, 84
: , : , :
69conjecture
proveit.numbers.absolute_value.abs_non_neg_elim
70instantiation99, 247
:
71conjecture
proveit.numbers.numerals.decimals.posnat9
72conjecture
proveit.numbers.exponentiation.exp_pos_less
73instantiation254, 233, 85
: , : , :
74instantiation254, 86, 87
: , : , :
75instantiation131, 88, 89
: , :
76instantiation160, 103
:
77instantiation173, 90, 91, 92
: , : , : , :
78instantiation254, 246, 93
: , : , :
79conjecture
80conjecture
81instantiation254, 244, 94
: , : , :
82conjecture
proveit.numbers.number_sets.complex_numbers.zero_is_complex
83instantiation254, 249, 95
: , : , :
84instantiation146, 96, 97
: , : , :
85instantiation254, 249, 98
: , : , :
86conjecture
proveit.numbers.number_sets.real_numbers.real_pos_within_real
87conjecture
proveit.numbers.number_sets.real_numbers.pi_is_real_pos
88instantiation99, 134
:
89instantiation100, 101
: , :
90instantiation102, 103, 104
: , :
91instantiation105, 195, 106, 107, 108
: , : , : , :
92conjecture
proveit.numbers.numerals.decimals.mult_3_3
93conjecture
proveit.numbers.numerals.decimals.nat5
94instantiation254, 233, 109
: , : , :
95instantiation254, 246, 110
: , : , :
96instantiation190, 111, 147
: , : , :
97instantiation112, 256, 113
: , :
98instantiation254, 246, 195
: , : , :
99conjecture
proveit.numbers.number_sets.natural_numbers.natural_lower_bound
100theorem
proveit.logic.booleans.conjunction.left_from_and
101conjecture
proveit.numbers.number_sets.real_numbers.pi_between_3_and_4
102conjecture
proveit.numbers.exponentiation.exp_nat_pos_expansion
103conjecture
proveit.numbers.numerals.decimals.posnat2
104instantiation254, 244, 114
: , : , :
105conjecture
proveit.core_expr_types.operations.operands_substitution_via_tuple
106instantiation115, 195
: , :
107instantiation210
: , :
108instantiation116
:
109instantiation254, 249, 117
: , : , :
110conjecture
proveit.numbers.numerals.decimals.nat9
111modus ponens118, 119
112conjecture
proveit.numbers.modular.int_mod_elimination
113instantiation123, 124, 125, 248, 120
: , : , :
114instantiation254, 233, 121
: , : , :
115conjecture
proveit.core_expr_types.tuples.range_from1_len_typical_eq
116conjecture
proveit.numbers.numerals.decimals.reduce_2_repeats
117instantiation254, 246, 122
: , : , :
118conjecture
proveit.physics.quantum.QPE._alpha_ideal_case
119instantiation123, 124, 125, 140, 126
: , : , :
120instantiation131, 127, 128
: , :
121instantiation254, 249, 129
: , : , :
122conjecture
proveit.numbers.numerals.decimals.nat4
123conjecture
proveit.numbers.number_sets.integers.in_interval
124conjecture
proveit.numbers.number_sets.integers.zero_is_int
125instantiation130, 250, 166
: , :
126instantiation131, 132, 133
: , :
127instantiation190, 132, 147
: , : , :
128instantiation190, 133, 147
: , : , :
129instantiation254, 246, 134
: , : , :
130conjecture
131theorem
proveit.logic.booleans.conjunction.and_if_both
132instantiation135, 245, 158, 213, 136, 137, 138*
: , : , :
133instantiation139, 140, 250, 166, 141, 142
: , : , :
134conjecture
proveit.numbers.numerals.decimals.nat3
135conjecture
proveit.numbers.multiplication.weak_bound_via_right_factor_bound
136instantiation143, 158, 222, 159
: , : , :
137instantiation144, 150
: , :
138instantiation145, 238
:
139conjecture
140instantiation146, 248, 147
: , : , :
141instantiation148, 245, 213, 222, 149, 150, 221*
: , : , :
142instantiation151, 152, 153
: , :
143conjecture
proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
144conjecture
proveit.numbers.ordering.relax_less
145conjecture
proveit.numbers.multiplication.mult_zero_right
146theorem
proveit.logic.equality.sub_left_side_into
147instantiation154, 245, 213, 224, 155, 156*
: , : , :
148conjecture
proveit.numbers.multiplication.strong_bound_via_right_factor_bound
149instantiation157, 158, 222, 159
: , : , :
150instantiation160, 256
:
151conjecture
proveit.numbers.ordering.relax_equal_to_less_eq
152instantiation254, 233, 161
: , : , :
153instantiation214
:
154conjecture
proveit.numbers.multiplication.left_mult_eq_real
155instantiation162, 163
: , :
156instantiation190, 164, 165
: , : , :
157conjecture
proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
158conjecture
proveit.numbers.number_sets.real_numbers.zero_is_real
159axiom
proveit.physics.quantum.QPE._phase_in_interval
160conjecture
proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
161instantiation254, 249, 166
: , : , :
162theorem
proveit.logic.equality.equals_reversal
163instantiation167, 234, 178, 168, 179, 169*, 170*
: , : , :
164instantiation190, 171, 172
: , : , :
165instantiation173, 174, 175, 176
: , : , : , :
166instantiation177, 239
:
167conjecture
168instantiation190, 178, 179
: , : , :
169instantiation180, 212
:
170instantiation218, 181, 182
: , : , :
171instantiation183, 207, 208, 184, 185
: , : , : , : , :
172instantiation218, 186, 187
: , : , :
173conjecture
proveit.logic.equality.four_chain_transitivity
174instantiation228, 188
: , : , :
175instantiation228, 189
: , : , :
176instantiation237, 208
:
177conjecture
proveit.numbers.negation.int_closure
178conjecture
proveit.numbers.number_sets.rational_numbers.zero_is_rational
179instantiation190, 191, 192
: , : , :
180conjecture
181instantiation193, 194, 195, 247, 196, 197, 200, 198, 212
: , : , : , : , : , :
182instantiation199, 212, 200, 201
: , : , :
183conjecture
proveit.numbers.division.mult_frac_cancel_numer_left
184instantiation254, 203, 202
: , : , :
185instantiation254, 203, 204
: , : , :
186instantiation228, 205
: , : , :
187instantiation228, 206
: , : , :
188instantiation230, 207
:
189instantiation230, 208
:
190theorem
proveit.logic.equality.sub_right_side_into
191instantiation209, 248
:
192assumption
193conjecture
194axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
195conjecture
proveit.numbers.numerals.decimals.nat2
196conjecture
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
197instantiation210
: , :
198instantiation211, 212
:
199conjecture
200instantiation254, 244, 213
: , : , :
201instantiation214
:
202instantiation254, 216, 215
: , : , :
203conjecture
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
204instantiation254, 216, 217
: , : , :
205instantiation218, 219, 220
: , : , :
206instantiation228, 221
: , : , :
207instantiation254, 244, 222
: , : , :
208instantiation254, 244, 223
: , : , :
209axiom
proveit.physics.quantum.QPE._delta_b_def
210conjecture
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
211conjecture
proveit.numbers.negation.complex_closure
212instantiation254, 244, 224
: , : , :
213conjecture
proveit.physics.quantum.QPE._phase_is_real
214axiom
proveit.logic.equality.equals_reflexivity
215instantiation254, 226, 225
: , : , :
216conjecture
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
217instantiation254, 226, 227
: , : , :
218axiom
proveit.logic.equality.equals_transitivity
219instantiation228, 229
: , : , :
220instantiation230, 238
:
221instantiation231, 238
:
222instantiation254, 233, 232
: , : , :
223instantiation254, 233, 241
: , : , :
224instantiation254, 233, 234
: , : , :
225instantiation254, 235, 256
: , : , :
226conjecture
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
227instantiation254, 235, 236
: , : , :
228axiom
proveit.logic.equality.substitution
229instantiation237, 238
:
230conjecture
proveit.numbers.division.frac_one_denom
231conjecture
proveit.numbers.multiplication.elim_one_right
232instantiation254, 249, 239
: , : , :
233conjecture
proveit.numbers.number_sets.real_numbers.rational_within_real
234instantiation240, 241, 242, 243
: , :
235conjecture
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
236conjecture
proveit.numbers.numerals.decimals.posnat1
237conjecture
proveit.numbers.multiplication.elim_one_left
238instantiation254, 244, 245
: , : , :
239instantiation254, 246, 247
: , : , :
240conjecture
proveit.numbers.division.div_rational_closure
241instantiation254, 249, 248
: , : , :
242instantiation254, 249, 250
: , : , :
243instantiation251, 256
:
244conjecture
proveit.numbers.number_sets.complex_numbers.real_within_complex
245instantiation252, 253, 256
: , : , :
246conjecture
proveit.numbers.number_sets.integers.nat_within_int
247theorem
proveit.numbers.numerals.decimals.nat1
248conjecture
proveit.physics.quantum.QPE._best_round_is_int
249conjecture
proveit.numbers.number_sets.rational_numbers.int_within_rational
250instantiation254, 255, 256
: , : , :
251conjecture
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
252theorem
proveit.logic.sets.inclusion.unfold_subset_eq
253instantiation257, 258
: , :
254theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
255conjecture
proveit.numbers.number_sets.integers.nat_pos_within_int
256conjecture
proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
257theorem
proveit.logic.sets.inclusion.relax_proper_subset
258conjecture
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements