logo
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 = (
        frac(one, Exp(two, Add(one, _t))).deduce_bound(
        _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  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
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  ⊢  
 proveit.numbers.addition.elim_zero_right
40conjecture  ⊢  
 proveit.numbers.addition.commutation
41conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
42instantiation270  ⊢  
  : , :
43conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_23
44instantiation73, 58, 309, 161, 59, 60*, 61*, 62*  ⊢  
  : , : , : , :
45conjecture  ⊢  
 proveit.numbers.addition.add_real_closure_bin
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  ⊢  
 proveit.numbers.addition.add_rational_closure_bin
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  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_13
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  ⊢  
 proveit.numbers.addition.disassociation
101instantiation270  ⊢  
  : , :
102instantiation332, 321, 125  ⊢  
  : , : , :
103conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_12
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  ⊢  
 proveit.numbers.ordering.less_eq_add_right_strong
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  ⊢  
 proveit.numbers.addition.rational_pair_addition
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  ⊢