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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import l, x, N, defaults
from proveit.numbers import (
zero, one, two, Div, greater_eq, Less, Mult, Neg, subtract)
from proveit.numbers.modular import mod_abs_x_reduce_to_abs_x
from proveit.physics.quantum.QPE import (
_t_in_natural_pos, _two_pow_t, _two_pow__t_minus_one,
_two_pow_t_is_nat_pos)

In [2]:
%proving _modabs_in_full_domain_simp

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

defaults.assumptions:
In [4]:
# for convenience
l_membership = _modabs_in_full_domain_simp.condition

l_membership:

We plan to instantiate the following mod_abs_x_reduce_to_abs_x theorem with $x: \ell$ and $N = 2^t$, the challenging piece of which is to establish that $|\ell|\le\frac{2^t}{2}=2^{t-1}$:

In [5]:
mod_abs_x_reduce_to_abs_x


Establish an upper bound on $|\ell|$, and along the way establish some properties of the $\ell$ bounds $2^{t-1}$ and $-2^{t-1}+1$ so their absolute values will eventually be (automatically) simplified and so we can also evaluate a Max() on the values.

In [6]:
from proveit.numbers.absolute_value import weak_upper_bound_asym_interval
weak_upper_bound_asym_interval

In [7]:
temp_bound_01 = _two_pow__t_minus_one.deduce_bound(_t_in_natural_pos.derive_element_lower_bound())

temp_bound_01:

From temp_bound_01, we can also automatically derive $-2^{t-1}\ge -1$ and $-2^{t-1}+1\ge 0$ as needed (through canonical forms).

In [8]:
# temp_bound_02 = temp_bound_01.left_mult_both_sides(Neg(one))

In [9]:
# temp_bound_03 = temp_bound_02.right_add_both_sides(one)

In [10]:
# Want to explicitly establish this, so the eventual Max() evaluation
# will go through in the instantiation of abs_l_max_bound further below
Less(subtract(temp_bound_01.lhs, one), temp_bound_01.lhs).prove()


Since we know $-2^{t-1}+1 \le 0$ and $0 < 2^{t-1}-1 < 2^{t-1}$, when we instantiate the weak_upper_bound_asym_interval theorem, the absolute values are simplified, and since we have pre-established the relative size of $2^{t-1}-1$ and $2^{t-1}$, the Max() operation can be simplified:

In [11]:
from proveit import a, b, c
_a_sub, _b_sub, _c_sub = (
l,
l_membership.domain.lower_bound,
l_membership.domain.upper_bound)
abs_l_max_bound = weak_upper_bound_asym_interval.instantiate(
{a: _a_sub, b: _b_sub, c: _c_sub})

abs_l_max_bound:

Now we're ready to instantiate the mod_abs_x_reduce_to_abs_x theorem

In [12]:
# here we set auto_simplify=False, else we simply obtain the unhelpful |ell|=|ell|
mod_abs_x_reduce_to_abs_x.instantiate({x: l, N: _two_pow_t}, auto_simplify=False)

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

In [13]:
%qed

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

Out[13]:
step typerequirementsstatement
0generalization1
1instantiation2, 12, 3, 4
: , :
2conjecture
proveit.numbers.modular.mod_abs_x_reduce_to_abs_x
3instantiation208, 5, 6
: , : , :
4instantiation7, 8, 9
: , : , :
5conjecture
proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
6instantiation208, 10, 168
: , : , :
7theorem
proveit.logic.equality.sub_right_side_into
8instantiation11, 12, 13, 86, 14, 15*
: , : , :
9instantiation131, 121, 16, 17
: , : , : , :
10conjecture
proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
11conjecture
proveit.numbers.absolute_value.weak_upper_bound_asym_interval
12instantiation208, 197, 18
: , : , :
13instantiation208, 197, 19
: , : , :
14instantiation20, 21, 22
: , :
15instantiation115, 23, 24
: , : , :
16instantiation146, 25
: , : , :
17instantiation144, 26
: , :
18instantiation208, 204, 27
: , : , :
19instantiation208, 204, 51
: , : , :
20theorem
proveit.logic.booleans.conjunction.and_if_both
21instantiation28, 51, 111, 39
: , : , :
22instantiation29, 51, 111, 39
: , : , :
23instantiation70, 210, 30, 31, 32, 33
: , : , : , :
24instantiation115, 34, 35
: , : , :
25instantiation146, 167
: , : , :
26instantiation36, 138, 179, 166, 37*
: , :
27instantiation208, 38, 39
: , : , :
28conjecture
proveit.numbers.number_sets.integers.interval_lower_bound
29conjecture
proveit.numbers.number_sets.integers.interval_upper_bound
30instantiation135
: , :
31instantiation135
: , :
32instantiation40, 41, 42*
:
33instantiation43, 44
:
34instantiation45, 94, 86
: , :
35instantiation46, 86, 94, 47*
: , :
36conjecture
proveit.numbers.division.div_as_mult
37instantiation115, 48, 49
: , : , :
38instantiation50, 51, 111
: , :
39assumption
40conjecture
proveit.numbers.absolute_value.abs_neg_elim
41instantiation52, 76, 176, 86, 53, 54*, 55*
: , : , :
42instantiation56, 64, 164, 57*
: , :
43conjecture
proveit.numbers.absolute_value.abs_non_neg_elim
44instantiation90, 58
: , :
45conjecture
proveit.numbers.ordering.max_bin_args_commute
46axiom
proveit.numbers.ordering.max_def_bin
47instantiation115, 59, 60
: , : , :
48instantiation146, 61
: , : , :
49instantiation62, 138, 63
: , :
50conjecture
proveit.numbers.number_sets.integers.int_interval_within_int
51instantiation152, 88, 196
: , :
52conjecture
53instantiation171, 118
:
54instantiation157, 164, 64
: , :
55instantiation115, 65, 66
: , : , :
56conjecture
proveit.numbers.negation.distribute_neg_through_binary_sum
57instantiation67, 68
:
58instantiation69, 118
:
59instantiation70, 210, 71, 72, 73, 74
: , : , : , :
60instantiation75, 123, 203, 125
: , : , : , : , :
61instantiation161, 162, 207, 167*
: , :
62conjecture
proveit.numbers.multiplication.commutation
63instantiation148, 164, 179, 166
: , :
64instantiation208, 188, 76
: , : , :
65instantiation115, 77, 78
: , : , :
66instantiation79, 127, 104
: , :
67conjecture
proveit.numbers.negation.double_negation
68instantiation208, 188, 86
: , : , :
69conjecture
proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
70axiom
proveit.core_expr_types.operations.operands_substitution
71instantiation135
: , :
72instantiation135
: , :
73instantiation80, 87
: , :
74instantiation81, 82
: , :
75axiom
proveit.core_expr_types.conditionals.true_case_reduction
76instantiation208, 197, 83
: , : , :
77instantiation146, 121
: , : , :
78instantiation146, 84
: , : , :
79conjecture
80conjecture
proveit.core_expr_types.conditionals.satisfied_condition_reduction
81conjecture
proveit.core_expr_types.conditionals.dissatisfied_condition_reduction
82instantiation85, 94, 86, 87
: , :
83instantiation208, 204, 88
: , : , :
84instantiation146, 121
: , : , :
85conjecture
proveit.numbers.ordering.not_less_from_less_eq
86instantiation208, 197, 89
: , : , :
87instantiation90, 91
: , :
88instantiation92, 111
:
89instantiation208, 204, 111
: , : , :
90conjecture
proveit.numbers.ordering.relax_less
91instantiation93, 94, 95, 176, 96, 97*, 98*
: , : , :
92conjecture
proveit.numbers.negation.int_closure
93conjecture
94instantiation208, 197, 99
: , : , :
95conjecture
proveit.numbers.number_sets.real_numbers.zero_is_real
96conjecture
proveit.numbers.numerals.decimals.less_0_1
97instantiation131, 100, 101, 102
: , : , : , :
98instantiation131, 103, 104, 105
: , : , : , :
99instantiation208, 204, 106
: , : , :
100instantiation115, 107, 108
: , : , :
101instantiation139
:
102instantiation144, 114
: , :
103instantiation115, 109, 110
: , : , :
104instantiation139
:
105instantiation144, 121
: , :
106instantiation152, 111, 154
: , :
107instantiation146, 114
: , : , :
108instantiation115, 112, 113
: , : , :
109instantiation146, 114
: , : , :
110instantiation115, 116, 117
: , : , :
111instantiation208, 169, 118
: , : , :
112instantiation122, 203, 210, 123, 124, 125, 119, 127, 159
: , : , : , : , : , :
113instantiation120, 123, 210, 125, 124, 127, 159
: , : , : , :
114instantiation146, 121
: , : , :
115axiom
proveit.logic.equality.equals_transitivity
116instantiation122, 203, 210, 123, 124, 125, 164, 127, 159
: , : , : , : , : , :
117instantiation126, 164, 127, 128
: , : , :
118instantiation129, 210, 130
: , :
119conjecture
proveit.numbers.number_sets.complex_numbers.zero_is_complex
120conjecture
121instantiation131, 132, 133, 134
: , : , : , :
122conjecture
123axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
124instantiation135
: , :
125conjecture
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
126conjecture
127instantiation136, 137, 138
: , :
128instantiation139
:
129conjecture
proveit.numbers.exponentiation.exp_natpos_closure
130instantiation140, 141, 142
:
131conjecture
proveit.logic.equality.four_chain_transitivity
132instantiation146, 143
: , : , :
133instantiation144, 145
: , :
134instantiation146, 147
: , : , :
135conjecture
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
136conjecture
proveit.numbers.multiplication.mult_complex_closure_bin
137instantiation148, 164, 149, 150
: , :
138instantiation208, 188, 151
: , : , :
139axiom
proveit.logic.equality.equals_reflexivity
140conjecture
proveit.numbers.number_sets.integers.nonneg_int_is_natural
141instantiation152, 153, 154
: , :
142instantiation155, 156
: , :
143instantiation157, 158, 159
: , :
144theorem
proveit.logic.equality.equals_reversal
145instantiation160, 179, 173, 172, 166
: , : , :
146axiom
proveit.logic.equality.substitution
147instantiation161, 162, 207
: , :
148conjecture
proveit.numbers.division.div_complex_closure
149instantiation163, 179, 164
: , :
150instantiation165, 166, 167
: , : , :
151instantiation180, 181, 168
: , : , :
152conjecture
153instantiation208, 169, 182
: , : , :
154instantiation208, 170, 200
: , : , :
155conjecture
156instantiation171, 182
:
157conjecture
158instantiation208, 188, 172
: , : , :
159instantiation208, 188, 173
: , : , :
160conjecture
proveit.numbers.exponentiation.product_of_real_powers
161conjecture
proveit.numbers.exponentiation.neg_power_as_div
162instantiation208, 174, 175
: , : , :
163conjecture
proveit.numbers.exponentiation.exp_complex_closure
164instantiation208, 188, 176
: , : , :
165theorem
proveit.logic.equality.sub_left_side_into
166instantiation177, 202
:
167instantiation178, 179
:
168conjecture
proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
169conjecture
proveit.numbers.number_sets.integers.nat_pos_within_int
170conjecture
proveit.numbers.number_sets.integers.neg_int_within_int
171conjecture
proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
172instantiation180, 181, 182
: , : , :
173instantiation208, 183, 184
: , : , :
174conjecture
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
175instantiation208, 185, 186
: , : , :
176instantiation208, 197, 187
: , : , :
177conjecture
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
178conjecture
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
179instantiation208, 188, 189
: , : , :
180theorem
proveit.logic.sets.inclusion.unfold_subset_eq
181instantiation190, 191
: , :
182axiom
proveit.physics.quantum.QPE._t_in_natural_pos
183conjecture
proveit.numbers.number_sets.real_numbers.real_neg_within_real
184instantiation208, 192, 193
: , : , :
185conjecture
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
186instantiation208, 194, 195
: , : , :
187instantiation208, 204, 196
: , : , :
188conjecture
proveit.numbers.number_sets.complex_numbers.real_within_complex
189instantiation208, 197, 198
: , : , :
190theorem
proveit.logic.sets.inclusion.relax_proper_subset
191conjecture
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
192conjecture
proveit.numbers.number_sets.real_numbers.rational_neg_within_real_neg
193instantiation208, 199, 200
: , : , :
194conjecture
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
195instantiation208, 201, 202
: , : , :
196instantiation208, 209, 203
: , : , :
197conjecture
proveit.numbers.number_sets.real_numbers.rational_within_real
198instantiation208, 204, 205
: , : , :
199conjecture
proveit.numbers.number_sets.rational_numbers.neg_int_within_rational_neg
200instantiation206, 207
:
201conjecture
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
202conjecture
proveit.numbers.numerals.decimals.posnat2
203theorem
proveit.numbers.numerals.decimals.nat1
204conjecture
proveit.numbers.number_sets.rational_numbers.int_within_rational
205instantiation208, 209, 210
: , : , :
206conjecture
proveit.numbers.negation.int_neg_closure
207conjecture
proveit.numbers.numerals.decimals.posnat1
208theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
209conjecture
proveit.numbers.number_sets.integers.nat_within_int
210conjecture
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements