logo

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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, n, x, defaults
from proveit.logic import Forall, InSet, NotEquals, Set
from proveit.numbers import (
        zero, one, Add, IntervalOO, Less, Neg, Real)
from proveit.numbers.number_sets.real_numbers import (
        not_int_if_not_int_in_interval)
from proveit.physics.quantum.QPE import (
        _b_floor, _b_round, _best_floor_is_int, _best_round_is_int,
        _delta_b, _delta_b_in_interval, _delta_b_is_real,
        _delta_b_not_eq_scaledNonzeroInt, _t, _t_in_natural_pos,
       _two_pow_t, _two_pow_t_is_nat_pos, _two_pow_t_minus_one_is_nat_pos)
In [2]:
%proving _non_int_delta_b_diff
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_non_int_delta_b_diff:
(see dependencies)
In [3]:
defaults.assumptions = _non_int_delta_b_diff.all_conditions()
defaults.assumptions:
In [4]:
_delta_b_in_interval
 ⊢  
In [5]:
# should be an automatic incidental derivation; but we want the labeled result
_delta_b_in_interval_inst = _delta_b_in_interval.instantiate()
_delta_b_in_interval_inst:  ⊢  

Some convenient, short-cut labelings:

In [6]:
delta_diff = _non_int_delta_b_diff.instance_expr.element
delta_diff:
In [7]:
neg_ell_over_two_pow_t = delta_diff.operands[1]
neg_ell_over_two_pow_t:
In [8]:
ell_in_full_domain = defaults.assumptions[1]
ell_in_full_domain:

Some Domain Facts (imported above and listed here for clarity)

In [9]:
display(_t_in_natural_pos)
display(_two_pow_t_is_nat_pos)
display(_two_pow_t_minus_one_is_nat_pos)
display(_best_floor_is_int)
display(_best_round_is_int)
display(_delta_b_is_real)
 ⊢  
 ⊢  
 ⊢  
 ⊢  
 ⊢  
 ⊢  

The $2^{t-1}\in\mathbb{N}^{+}$ is needed for establishing that the assumed $\ell$ domain consists of integers.
The last three involving $b$ automatically give us $\forall_{b\in\{b_{f}, b_{r}\}}\left[\delta_{b}\in\mathbb{R}\right]$.

Upper & Lower Bounds on $\ell$

In [10]:
ell_upper_bound = ell_in_full_domain.derive_element_upper_bound()
ell_upper_bound:  ⊢  
In [11]:
ell_lower_bound = ell_in_full_domain.derive_element_lower_bound()
ell_lower_bound:  ⊢  

Upper & Lower Bounds on $\delta_{b}$

In [12]:
delta_b_upper_bound = _delta_b_in_interval_inst.derive_element_upper_bound()
delta_b_upper_bound:  ⊢  
In [13]:
delta_b_lower_bound = _delta_b_in_interval_inst.derive_element_lower_bound()
delta_b_lower_bound:  ⊢  

Deducing Bounds on $\delta_{b} - \frac{\ell}{2^t}$

In [14]:
delta_diff_lower_bound = (
        delta_diff.deduce_bound(
        [ell_upper_bound, delta_b_lower_bound.reversed()]))
delta_diff_lower_bound: ,  ⊢  
In [15]:
delta_diff_upper_bound_01 = (
        delta_diff.deduce_bound(
        [ell_lower_bound.reversed(), delta_b_upper_bound]))
delta_diff_upper_bound_01: ,  ⊢  
In [16]:
delta_diff_upper_bound_02 = (
        delta_diff_upper_bound_01.inner_expr().rhs.operands[1].
        operand.distribute())
delta_diff_upper_bound_02: ,  ⊢  
In [17]:
Less(delta_diff_upper_bound_02.rhs, one).prove()
 ⊢  
In [18]:
# One might think we don't need this explicitly, but we need it for one of the final steps later
InSet(delta_diff, IntervalOO(Neg(one), one)).prove()
,  ⊢  

Now use the QPE theorem _delta_b_not_eq_scaledNonzeroInt to deduce that $\delta_{b}-\frac{\ell}{2^t} \ne 0$:

In [19]:
_delta_b_not_eq_scaledNonzeroInt
 ⊢  
In [20]:
_delta_b_not_eq_scaledNonzeroInt_inst = _delta_b_not_eq_scaledNonzeroInt.instantiate()
_delta_b_not_eq_scaledNonzeroInt_inst: , ,  ⊢  
In [21]:
NotEquals(Add(_delta_b, neg_ell_over_two_pow_t), zero).prove()
, ,  ⊢  

Instantiate one last useful theorem: $\delta_{b}-\frac{\ell}{2^t}\in(-1, 1)$ cannot be an integer if $\delta_{b}-\frac{\ell}{2^t}\ne 0$:

In [22]:
not_int_if_not_int_in_interval
 ⊢  
In [23]:
not_int_if_not_int_in_interval_inst = (
        not_int_if_not_int_in_interval.instantiate(
                {n: zero, x: delta_diff}))
not_int_if_not_int_in_interval_inst: , ,  ⊢  
_non_int_delta_b_diff may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [24]:
%qed

proveit.physics.quantum.QPE._non_int_delta_b_diff has been proven.
Out[24]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation2, 3, 4, 5, ,  ⊢  
  : , :
2conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.not_int_if_not_int_in_interval
3conjecture  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
4instantiation6, 7, 8, 9, 10,  ⊢  
  : , : , :
5instantiation11, 12, ,  ⊢  
  : , :
6conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.in_IntervalOO
7instantiation141, 13, 207  ⊢  
  : , :
8instantiation220, 221, 56  ⊢  
  : , : , :
9instantiation141, 62, 65,  ⊢  
  : , :
10instantiation14, 15, 16,  ⊢  
  : , :
11conjecture  ⊢  
 proveit.numbers.addition.subtraction.nonzero_difference_if_different
12instantiation17, 98, 127, 18, ,  ⊢  
  : , :
13conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
14theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
15instantiation21, 19, 20,  ⊢  
  : , : , :
16instantiation21, 22, 23,  ⊢  
  : , : , :
17conjecture  ⊢  
 proveit.physics.quantum.QPE._delta_b_not_eq_scaledNonzeroInt
18assumption  ⊢  
19instantiation26, 24, 25,  ⊢  
  : , : , :
20instantiation29, 196  ⊢  
  :
21theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
22instantiation26, 27, 28,  ⊢  
  : , : , :
23instantiation29, 155  ⊢  
  :
24instantiation64, 104, 30, 65, 31, 32*  ⊢  
  : , : , :
25instantiation33, 65, 104, 62, 34,  ⊢  
  : , : , :
26conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
27instantiation35, 36, 37, 38*,  ⊢  
  : , : , :
28instantiation39, 190, 232, 40, 191, 41, 216  ⊢  
  : , : , : , : , :
29conjecture  ⊢  
 proveit.numbers.addition.elim_zero_left
30instantiation215, 59  ⊢  
  :
31instantiation80, 82, 59, 42  ⊢  
  : , :
32instantiation43, 106, 44, 155, 45  ⊢  
  : , : , :
33conjecture  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
34instantiation46, 104, 119, 79  ⊢  
  : , : , :
35theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
36instantiation47, 48, 49,  ⊢  
  : , : , :
37instantiation50, 218, 51, 52, 155, 95, 149, 53*  ⊢  
  : , : , :
38instantiation174, 54, 55  ⊢  
  : , : , :
39conjecture  ⊢  
 proveit.numbers.addition.term_as_strong_upper_bound
40instantiation118, 56  ⊢  
  :
41instantiation57, 130  ⊢  
  :
42instantiation99, 112, 101, 111, 58, 103  ⊢  
  : , : , :
43conjecture  ⊢  
 proveit.numbers.addition.subtraction.negated_add
44instantiation230, 206, 59  ⊢  
  : , : , :
45instantiation174, 60, 92  ⊢  
  : , : , :
46conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
47conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
48instantiation61, 65, 62, 119, 63,  ⊢  
  : , : , :
49instantiation64, 119, 65, 66, 67  ⊢  
  : , : , :
50conjecture  ⊢  
 proveit.numbers.division.distribute_frac_through_sum
51instantiation204  ⊢  
  : , :
52instantiation230, 206, 68  ⊢  
  : , : , :
53instantiation69, 94, 95, 149, 76*  ⊢  
  : , :
54instantiation157, 70  ⊢  
  : , : , :
55instantiation174, 71, 72  ⊢  
  : , : , :
56instantiation73, 232, 190, 191, 74  ⊢  
  : , : , : , : , :
57conjecture  ⊢  
 proveit.numbers.negation.real_neg_closure
58instantiation75, 163, 201, 145  ⊢  
  : , : , :
59instantiation128, 111, 112, 149  ⊢  
  : , :
60instantiation157, 76  ⊢  
  : , : , :
61conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
62instantiation77, 104, 119, 79  ⊢  
  : , : , :
63instantiation78, 104, 119, 79  ⊢  
  : , : , :
64conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_right_term_bound
65instantiation215, 82  ⊢  
  :
66instantiation215, 81  ⊢  
  :
67instantiation80, 81, 82, 83  ⊢  
  : , :
68instantiation230, 223, 84  ⊢  
  : , : , :
69conjecture  ⊢  
 proveit.numbers.division.neg_frac_neg_numerator
70instantiation85, 86, 108, 87*  ⊢  
  : , :
71instantiation189, 232, 225, 190, 88, 191, 106, 91  ⊢  
  : , : , : , : , : , :
72instantiation89, 190, 225, 232, 191, 90, 106, 91, 92*  ⊢  
  : , : , : , : , : , :
73conjecture  ⊢  
 proveit.numbers.addition.add_nat_pos_from_nonneg
74conjecture  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
75conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
76instantiation93, 94, 95, 149, 96*  ⊢  
  : , :
77conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
78conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound
79instantiation97, 98  ⊢  
  :
80conjecture  ⊢  
 proveit.numbers.negation.negated_weak_bound
81instantiation128, 100, 112, 149  ⊢  
  : , :
82instantiation128, 101, 112, 149  ⊢  
  : , :
83instantiation99, 112, 100, 101, 102, 103  ⊢  
  : , : , :
84instantiation230, 228, 181  ⊢  
  : , : , :
85conjecture  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
86instantiation230, 206, 104  ⊢  
  : , : , :
87instantiation105, 106  ⊢  
  :
88instantiation204  ⊢  
  : , :
89conjecture  ⊢  
 proveit.numbers.addition.association
90instantiation204  ⊢  
  : , :
91instantiation107, 108  ⊢  
  :
92instantiation109, 229, 219, 110*  ⊢  
  : , : , : , :
93conjecture  ⊢  
 proveit.numbers.division.div_as_mult
94instantiation230, 206, 111  ⊢  
  : , : , :
95instantiation230, 206, 112  ⊢  
  : , : , :
96instantiation174, 113, 114  ⊢  
  : , : , :
97conjecture  ⊢  
 proveit.physics.quantum.QPE._delta_b_in_interval
98assumption  ⊢  
99conjecture  ⊢  
 proveit.numbers.division.weak_div_from_numer_bound__pos_denom
100instantiation230, 223, 115  ⊢  
  : , : , :
101instantiation230, 223, 116  ⊢  
  : , : , :
102instantiation117, 163, 201, 145  ⊢  
  : , : , :
103instantiation118, 184  ⊢  
  :
104instantiation215, 119  ⊢  
  :
105conjecture  ⊢  
 proveit.numbers.negation.double_negation
106instantiation230, 206, 119  ⊢  
  : , : , :
107conjecture  ⊢  
 proveit.numbers.negation.complex_closure
108instantiation230, 206, 120  ⊢  
  : , : , :
109conjecture  ⊢  
 proveit.numbers.addition.rational_pair_addition
110instantiation174, 121, 122  ⊢  
  : , : , :
111instantiation220, 221, 212  ⊢  
  : , : , :
112instantiation220, 221, 184  ⊢  
  : , : , :
113instantiation157, 123  ⊢  
  : , : , :
114instantiation124, 187, 125, 205, 139, 126*  ⊢  
  : , : , :
115instantiation230, 228, 163  ⊢  
  : , : , :
116instantiation230, 228, 127  ⊢  
  : , : , :
117conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
118conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
119instantiation128, 216, 202, 139  ⊢  
  : , :
120instantiation230, 129, 130  ⊢  
  : , : , :
121instantiation168, 225, 131, 132, 133, 134  ⊢  
  : , : , : , :
122instantiation135, 136, 137  ⊢  
  :
123instantiation138, 187, 214, 207, 139, 140*  ⊢  
  : , : , :
124conjecture  ⊢  
 proveit.numbers.exponentiation.product_of_real_powers
125instantiation141, 214, 207  ⊢  
  : , :
126instantiation174, 142, 143  ⊢  
  : , : , :
127instantiation230, 144, 145  ⊢  
  : , : , :
128conjecture  ⊢  
 proveit.numbers.division.div_real_closure
129conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
130instantiation146, 147, 148, 149  ⊢  
  : , :
131instantiation204  ⊢  
  : , :
132instantiation204  ⊢  
  : , :
133instantiation174, 150, 151  ⊢  
  : , : , :
134conjecture  ⊢  
 proveit.numbers.numerals.decimals.mult_2_2
135conjecture  ⊢  
 proveit.numbers.division.frac_cancel_complete
136instantiation230, 206, 152  ⊢  
  : , : , :
137instantiation167, 153  ⊢  
  :
138conjecture  ⊢  
 proveit.numbers.exponentiation.real_power_of_real_power
139instantiation167, 218  ⊢  
  :
140instantiation154, 195, 155, 156*  ⊢  
  : , :
141conjecture  ⊢  
 proveit.numbers.addition.add_real_closure_bin
142instantiation157, 158  ⊢  
  : , : , :
143instantiation159, 160, 182, 161*  ⊢  
  : , :
144instantiation162, 163, 201  ⊢  
  : , :
145assumption  ⊢  
146conjecture  ⊢  
 proveit.numbers.division.div_real_pos_closure
147instantiation230, 165, 164  ⊢  
  : , : , :
148instantiation230, 165, 166  ⊢  
  : , : , :
149instantiation167, 184  ⊢  
  :
150instantiation168, 225, 169, 170, 171, 172  ⊢  
  : , : , : , :
151conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_2_2
152instantiation230, 223, 173  ⊢  
  : , : , :
153conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat4
154conjecture  ⊢  
 proveit.numbers.multiplication.mult_neg_right
155instantiation230, 206, 216  ⊢  
  : , : , :
156instantiation186, 195  ⊢  
  :
157axiom  ⊢  
 proveit.logic.equality.substitution
158instantiation174, 175, 176  ⊢  
  : , : , :
159conjecture  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
160instantiation230, 177, 178  ⊢  
  : , : , :
161instantiation179, 187  ⊢  
  :
162conjecture  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
163instantiation180, 181, 229  ⊢  
  : , :
164instantiation230, 183, 182  ⊢  
  : , : , :
165conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
166instantiation230, 183, 184  ⊢  
  : , : , :
167conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
168axiom  ⊢  
 proveit.core_expr_types.operations.operands_substitution
169instantiation204  ⊢  
  : , :
170instantiation204  ⊢  
  : , :
171instantiation185, 187  ⊢  
  :
172instantiation186, 187  ⊢  
  :
173instantiation230, 228, 188  ⊢  
  : , : , :
174axiom  ⊢  
 proveit.logic.equality.equals_transitivity
175instantiation189, 190, 225, 232, 191, 192, 195, 196, 193  ⊢  
  : , : , : , : , : , :
176instantiation194, 195, 196, 197  ⊢  
  : , : , :
177conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
178instantiation230, 198, 199  ⊢  
  : , : , :
179conjecture  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
180conjecture  ⊢  
 proveit.numbers.addition.add_int_closure_bin
181instantiation200, 201  ⊢  
  :
182conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat1
183conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
184conjecture  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
185conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_left
186conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_right
187instantiation230, 206, 202  ⊢  
  : , : , :
188instantiation230, 231, 203  ⊢  
  : , : , :
189conjecture  ⊢  
 proveit.numbers.addition.disassociation
190axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
191conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
192instantiation204  ⊢  
  : , :
193instantiation230, 206, 205  ⊢  
  : , : , :
194conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_13
195instantiation230, 206, 214  ⊢  
  : , : , :
196instantiation230, 206, 207  ⊢  
  : , : , :
197instantiation208  ⊢  
  :
198conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
199instantiation230, 209, 210  ⊢  
  : , : , :
200conjecture  ⊢  
 proveit.numbers.negation.int_closure
201instantiation230, 211, 212  ⊢  
  : , : , :
202instantiation230, 223, 213  ⊢  
  : , : , :
203conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat4
204conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
205instantiation215, 214  ⊢  
  :
206conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
207instantiation215, 216  ⊢  
  :
208axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
209conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
210instantiation230, 217, 218  ⊢  
  : , : , :
211conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
212conjecture  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
213instantiation230, 228, 219  ⊢  
  : , : , :
214instantiation220, 221, 222  ⊢  
  : , : , :
215conjecture  ⊢  
 proveit.numbers.negation.real_closure
216instantiation230, 223, 224  ⊢  
  : , : , :
217conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
218conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat2
219instantiation230, 231, 225  ⊢  
  : , : , :
220theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
221instantiation226, 227  ⊢  
  : , :
222axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
223conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
224instantiation230, 228, 229  ⊢  
  : , : , :
225conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat2
226theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
227conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
228conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
229instantiation230, 231, 232  ⊢  
  : , : , :
230theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
231conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
232theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
*equality replacement requirements