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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, defaults
from proveit.logic import Forall, Set
from proveit.numbers import one, two, Add, Exp, frac, Less, LessEq, Neg, Mult
from proveit.physics.quantum.QPE import (
_b_floor, _b_round, _best_floor_is_int, _best_round_is_int,
_delta_b, _delta_b_floor, _delta_b_is_real, _delta_b_round,
_scaled_delta_b_floor_in_interval, _scaled_delta_b_round_in_interval,
_t, _t_in_natural_pos, _two_pow_t, _two_pow_t_is_nat_pos )

In [2]:
%proving _delta_b_in_interval

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

defaults.assumptions:
In [4]:
_two_pow_t_is_nat_pos

In [5]:
_scaled_delta_b_floor_in_interval

In [6]:
_best_floor_is_int

In [7]:
_delta_b_is_real

In [8]:
_delta_b_f_is_real = _delta_b_is_real.instantiate({b: _b_floor})

_delta_b_f_is_real:
In [9]:
delta_b_f_interval_membership = (
_scaled_delta_b_floor_in_interval.
derive_rescaled_membership(frac(one, _two_pow_t)))

delta_b_f_interval_membership:
In [10]:
_t_in_natural_pos

In [11]:
t_ge_one = _t_in_natural_pos.derive_element_lower_bound()

t_ge_one:
In [12]:
two_pow_t_ge_2 = _two_pow_t.deduce_bound(t_ge_one)

two_pow_t_ge_2:
In [13]:
one_over_two_pow_t_less_one_half = (
frac(one, _two_pow_t).deduce_bound(two_pow_t_ge_2))

one_over_two_pow_t_less_one_half:

Now it knows that $0 \leq \delta_{b_f} \leq 1/2$ via automation which is stronger than $\delta_{b_f} \in \left(-1/2, 1/2\right]$.

In [14]:
_scaled_delta_b_round_in_interval

In [15]:
_best_round_is_int

In [16]:
_delta_b_is_real.instantiate({b: _b_round})

In [17]:
with Mult.temporary_simplification_directives() as tmp_directives:
tmp_directives.distribute_fractions = True
delta_b_r_interval_membership = (
_scaled_delta_b_round_in_interval.
derive_rescaled_membership(frac(one, _two_pow_t)))

delta_b_r_interval_membership:
In [18]:
# for convenience
_two_pow__t_plus_one = delta_b_r_interval_membership.domain.upper_bound.denominator

_two_pow__t_plus_one:
In [19]:
t_less_t_plus_one = Less(_t, Add(one, _t)).prove()

t_less_t_plus_one:
In [20]:
_two_pow__t_plus_one_greater_two_pow_t = (
_two_pow__t_plus_one.deduce_bound(t_less_t_plus_one.reversed()))

_two_pow__t_plus_one_greater_two_pow_t:
In [21]:
one_over_two_pow__t_plus_one_less_one_over_two_pow_t = (
_two_pow__t_plus_one_greater_two_pow_t))

one_over_two_pow__t_plus_one_less_one_over_two_pow_t:

And we have already established that $\frac{1}{2^t} < \frac{1}{2}$. Thus we know that $\delta_{b_r} < \frac{1}{2}$ via automation.

And it follows that $-\frac{1}{2}\le-\frac{1}{2^t}$, and thus $-\frac{1}{2}<\delta_{b_r}$ via automation.

In [22]:
%qed

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

Out[22]:
step typerequirementsstatement
0instantiation1, 2, 3, 4, 5
: , : , : , :
1conjecture
proveit.logic.sets.enumeration.true_for_each_then_true_for_all
2reference331
3instantiation270
: , :
4instantiation7, 125, 243, 145, 6
: , : , :
5instantiation7, 125, 243, 158, 8
: , : , :
6instantiation11, 9, 10
: , :
7conjecture
proveit.numbers.number_sets.real_numbers.in_IntervalOC
8instantiation11, 12, 13
: , :
9instantiation28, 125, 58, 14, 15, 16*, 17*
: , : , :
10instantiation169, 18
: , :
11theorem
proveit.logic.booleans.conjunction.and_if_both
12instantiation35, 19, 20
: , : , :
13instantiation169, 21
: , :
14instantiation45, 145, 243
: , :
15instantiation115, 58, 145, 243, 22, 170
: , : , :
16instantiation185, 23, 24
: , : , :
17instantiation266, 25, 26
: , : , :
18instantiation35, 27, 143
: , : , :
19instantiation28, 29, 116, 30, 94, 31*, 32*
: , : , :
20instantiation33, 55, 72, 34
: , : , :
21instantiation35, 36, 37
: , : , :
22instantiation38, 58, 161, 44
: , : , :
23instantiation39, 102
:
24instantiation40, 102, 41
: , :
25instantiation100, 216, 331, 334, 217, 42, 121, 219, 102
: , : , : , : , : , :
26instantiation43, 219, 121, 105
: , : , :
27instantiation54, 58, 161, 44
: , : , :
28conjecture
29instantiation45, 125, 46
: , :
30instantiation332, 319, 47
: , : , :
31instantiation266, 48, 49
: , : , :
32instantiation188, 50, 51, 52
: , : , : , :
33conjecture
proveit.numbers.number_sets.real_numbers.interval_cc_lower_bound
34instantiation53, 55, 72, 56
: , : , :
35conjecture
proveit.numbers.ordering.transitivity_less_less_eq
36instantiation54, 55, 72, 56
: , : , :
37instantiation185, 57, 98
: , : , :
38conjecture
proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
39conjecture
40conjecture
41conjecture
proveit.numbers.number_sets.complex_numbers.zero_is_complex
42instantiation270
: , :
43conjecture
44instantiation73, 58, 309, 161, 59, 60*, 61*, 62*
: , : , : , :
45conjecture
46instantiation294, 116
:
47instantiation63, 64, 141
: , :
48instantiation266, 65, 66
: , : , :
49instantiation266, 67, 68
: , : , :
50instantiation266, 69, 70
: , : , :
51instantiation127
:
52instantiation150, 71
: , :
53conjecture
proveit.numbers.number_sets.real_numbers.relax_IntervalCO
54conjecture
proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
55instantiation294, 72
:
56instantiation73, 125, 243, 161, 74, 75*, 76*, 93*
: , : , : , :
57instantiation185, 77, 114
: , : , :
58conjecture
proveit.numbers.number_sets.real_numbers.zero_is_real
59conjecture
proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
60instantiation188, 78, 79, 80
: , : , : , :
61instantiation81, 138
:
62instantiation310, 138
:
63conjecture
64instantiation162, 262
: , :
65instantiation288, 149
: , : , :
66instantiation288, 99
: , : , :
67instantiation100, 334, 331, 216, 101, 217, 126, 102, 104
: , : , : , : , : , :
68instantiation82, 126, 102, 83
: , : , :
69instantiation266, 84, 85
: , : , :
70instantiation266, 86, 87
: , : , :
71instantiation288, 88
: , : , :
72instantiation332, 319, 89
: , : , :
73conjecture
proveit.numbers.number_sets.real_numbers.rescale_interval_co_membership
74conjecture
proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval
75instantiation188, 90, 91, 92
: , : , : , :
76instantiation296, 138, 219, 93*
: , :
77instantiation169, 94
: , :
78instantiation214, 334, 331, 216, 95, 217, 138, 306, 121
: , : , : , : , : , :
79instantiation266, 96, 97
: , : , :
80instantiation287, 121
:
81conjecture
proveit.numbers.multiplication.mult_zero_right
82conjecture
83instantiation127
:
84instantiation288, 98
: , : , :
85instantiation288, 99
: , : , :
86instantiation100, 334, 331, 216, 101, 217, 219, 102, 104
: , : , : , : , : , :
87instantiation103, 219, 104, 105
: , : , :
88instantiation266, 106, 107
: , : , :
89instantiation228, 320, 108, 109
: , :
90instantiation214, 334, 331, 216, 110, 217, 138, 306, 135
: , : , : , : , : , :
91instantiation266, 111, 112
: , : , :
92instantiation287, 135
:
93instantiation266, 113, 114
: , : , :
94instantiation115, 116, 117, 118, 119, 120
: , : , :
95instantiation270
: , :
96instantiation133, 216, 331, 334, 217, 134, 138, 306, 121
: , : , : , : , : , :
97instantiation288, 136
: , : , :
98instantiation266, 122, 123
: , : , :
99instantiation288, 124
: , : , :
100conjecture
101instantiation270
: , :
102instantiation332, 321, 125
: , : , :
103conjecture
104instantiation300, 126
:
105instantiation127
:
106instantiation288, 128
: , : , :
107instantiation210, 297, 129, 130, 131*
: , :
108instantiation332, 326, 132
: , : , :
109instantiation295, 157
:
110instantiation270
: , :
111instantiation133, 216, 331, 334, 217, 134, 138, 306, 135
: , : , : , : , : , :
112instantiation288, 136
: , : , :
113instantiation137, 138, 219
: , :
114instantiation172, 297, 241, 224, 191*, 151*
: , : , : , :
115conjecture
116instantiation332, 319, 139
: , : , :
117instantiation140, 243
: , :
118instantiation332, 319, 141
: , : , :
119instantiation142, 243, 161, 143, 144
: , : , :
120instantiation201, 163
:
121instantiation332, 321, 145
: , : , :
122instantiation288, 146
: , : , :
123instantiation147, 327, 318, 148*
: , : , : , :
124instantiation288, 149
: , : , :
125instantiation294, 243
:
126instantiation152, 219, 258
: , :
127axiom
proveit.logic.equality.equals_reflexivity
128instantiation150, 151
: , :
129instantiation152, 279, 306
: , :
130instantiation153, 331, 154, 241, 224
: , :
131instantiation266, 155, 156
: , : , :
132instantiation332, 269, 157
: , : , :
133conjecture
proveit.numbers.multiplication.association
134instantiation270
: , :
135instantiation332, 321, 158
: , : , :
136instantiation185, 159, 160
: , : , :
137conjecture
proveit.numbers.multiplication.commutation
138instantiation332, 321, 161
: , : , :
139instantiation162, 262, 192
: , :
140conjecture
proveit.numbers.multiplication.mult_real_closure_bin
141instantiation332, 283, 163
: , : , :
142conjecture
proveit.numbers.multiplication.weak_bound_via_right_factor_bound
143instantiation164, 165, 166, 167, 168
: , : , :
144instantiation169, 170
: , :
145instantiation183, 171
:
146instantiation172, 297, 241, 191*, 173*
: , : , : , :
147conjecture
148instantiation266, 174, 175
: , : , :
149instantiation288, 176
: , : , :
150theorem
proveit.logic.equality.equals_reversal
151instantiation177, 279, 314, 330, 242*
: , : , :
152conjecture
proveit.numbers.multiplication.mult_complex_closure_bin
153conjecture
proveit.numbers.multiplication.mult_not_eq_zero
154instantiation270
: , :
155instantiation288, 178
: , : , :
156instantiation266, 179, 180
: , : , :
157instantiation181, 331, 182
: , :
158instantiation183, 184
:
159instantiation185, 186, 187
: , : , :
160instantiation188, 189, 190, 191
: , : , : , :
161instantiation332, 319, 192
: , : , :
162conjecture
proveit.numbers.multiplication.mult_rational_closure_bin
163instantiation303, 304, 193
: , :
164conjecture
proveit.numbers.division.weak_div_from_denom_bound__all_pos
165instantiation332, 194, 195
: , : , :
166instantiation332, 196, 305
: , : , :
167instantiation332, 196, 197
: , : , :
168instantiation198, 299, 309, 322, 199, 200, 242*
: , : , :
169conjecture
proveit.numbers.ordering.relax_less
170instantiation201, 284
:
171conjecture
proveit.physics.quantum.QPE._best_floor_is_int
172conjecture
proveit.numbers.division.prod_of_fracs
173conjecture
proveit.numbers.numerals.decimals.mult_2_2
174instantiation250, 331, 202, 203, 204, 205
: , : , : , :
175instantiation206, 207, 241, 297, 208*, 209*
: , : , :
176instantiation210, 297, 306, 230, 211*
: , :
177conjecture
proveit.numbers.exponentiation.product_of_posnat_powers
178instantiation212, 279, 306, 275, 276, 230, 213*, 257*
: , : , :
179instantiation214, 334, 331, 216, 218, 217, 297, 219, 258
: , : , : , : , : , :
180instantiation215, 216, 331, 217, 218, 219, 258
: , : , : , :
181conjecture
proveit.numbers.exponentiation.exp_natpos_closure
182instantiation220, 334, 221
: , :
183conjecture
proveit.physics.quantum.QPE._delta_b_is_real
184conjecture
proveit.physics.quantum.QPE._best_round_is_int
185theorem
proveit.logic.equality.sub_right_side_into
186instantiation222, 297, 223, 224
: , : , : , : , :
187instantiation266, 225, 226
: , : , :
188conjecture
proveit.logic.equality.four_chain_transitivity
189instantiation288, 227
: , : , :
190instantiation288, 227
: , : , :
191instantiation310, 297
:
192instantiation228, 320, 229, 230
: , :
193instantiation332, 315, 231
: , : , :
194conjecture
proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
195instantiation332, 232, 334
: , : , :
196conjecture
proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
197instantiation332, 315, 324
: , : , :
198conjecture
proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
199conjecture
proveit.numbers.numerals.decimals.less_1_2
200instantiation233, 330
:
201conjecture
proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
202instantiation270
: , :
203instantiation270
: , :
204instantiation266, 234, 235
: , : , :
205conjecture
proveit.numbers.numerals.decimals.mult_4_4
206conjecture
proveit.numbers.division.frac_cancel_left
207instantiation332, 259, 236
: , : , :
208instantiation310, 237
:
209conjecture
proveit.numbers.numerals.decimals.mult_8_2
210conjecture
proveit.numbers.division.div_as_mult
211instantiation266, 238, 239
: , : , :
212conjecture
proveit.numbers.exponentiation.real_power_of_product
213instantiation240, 241, 314, 242*
: , :
214conjecture