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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, m, x, N, defaults
from proveit.logic import InSet
from proveit.numbers import two, Div, Floor, LessEq, ModAbs, Mult, Real, subtract
from proveit.numbers.modular import mod_abs_of_difference_bound, mod_abs_scaled
from proveit.numbers.rounding import floor_x_le_x
from proveit.physics.quantum.QPE import (
    _best_floor_def, _n_in_natural_pos, _phase,
    _phase_in_interval, _t_in_natural_pos, _two_pow_t,
    _two_pow_t__minus_one, _two_pow_t_minus_one_is_nat_pos)

%proving _precision_guarantee_lemma_02

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_precision_guarantee_lemma_02:
(see dependencies)

defaults.assumptions = _precision_guarantee_lemma_02.conditions

defaults.assumptions:

# for convenience
_thm_expr = _precision_guarantee_lemma_02.instance_expr

_thm_expr:

Import some basic local assumptions and local definitions

# some basic assumptions and definitions
display(_t_in_natural_pos)
display(_n_in_natural_pos)
display(_phase_in_interval)
display(_best_floor_def)

 ⊢  

 ⊢  

 ⊢  

 ⊢  

It is useful generally to establish that $2^{t}\varphi \ge \lfloor 2^{t}\varphi\rfloor$ (this is then used implicitly in some auto_simplification further below) (might be nice to convert this to a method of some sort in the Floor class?):

floor_x_le_x

 ⊢  

_x_sub = Mult(_two_pow_t, _phase)
floor_int_phase_bound = floor_x_le_x.instantiate({x: _x_sub}).reversed()

floor_int_phase_bound:

We gradually transform the assumed condition $|m-b|_{\text{mod}\;2^t} \le 2^{t-1}-1$ into the desired condition $|\frac{m}{2^{t}}-1|_{\text{mod}\;1} \le 2^{-n}$:

condition_01 = _precision_guarantee_lemma_02.condition.operands[1].prove()

condition_01:  ⊢  

condition_02 = (
    condition_01.inner_expr().lhs.value.operands[1].
    operand.substitute(_best_floor_def))

condition_02:  ⊢  

mod_abs_of_difference_bound

 ⊢  

Then for later auto-simplification to work well, we want to establish that $|\lfloor 2^{t}\varphi\rfloor - 2^{t}\varphi| \le 2^{t}/2$

div_mult_id = Div(_two_pow_t, two).cancelation(two)

div_mult_id:  ⊢  

The _two_pow_t_minus_one_is_nat_pos theorem, imported at the top, also lets us know that $\vdash 2^{t-1}\in\mathbb{N}$.

from proveit.numbers.rounding import real_minus_floor_interval
real_minus_floor_interval

 ⊢  

from proveit import x
from proveit.numbers import two, Exp
from proveit.physics.quantum.QPE import _t
_x_sub = Mult(Exp(two, _t), _phase)
real_minus_floor = real_minus_floor_interval.instantiate({x: _x_sub})

real_minus_floor:  ⊢  

from proveit.numbers import zero, one, Abs, IntervalCO
real_minus_floor_abs = InSet(Abs(real_minus_floor.element), IntervalCO(zero, one)).prove()

real_minus_floor_abs:  ⊢  

real_minus_floor_abs.inner_expr().element.reverse_difference(auto_simplify=False)

 ⊢  

Notice in the result of the following instantiation the ModAbs that would have appeared on the lhs with respect to $2^{t}$ has been automatically simplified to a non-modular (and non-absolute-value) expression:

_a_sub, _b_sub, _N_sub = (
    subtract(m, Mult(_two_pow_t, _phase)),
    subtract(m, Floor(Mult(_two_pow_t, _phase))),
    _two_pow_t)
condition_03 = mod_abs_of_difference_bound.instantiate(
        {a: _a_sub, b: _b_sub, N: _N_sub}).inner_expr().lhs.dividend.commute(0,1)

condition_03:  ⊢  

condition_04 = condition_03.inner_expr().lhs.commute(0, 1).with_styles(direction='normal')

condition_04:  ⊢  

But we also know from our work above that $2^{t}\varphi - \lfloor 2^{t}\varphi \rfloor < 1$, so Prove-It can now give us the following:

condition_05 = LessEq(condition_04.lhs, one).prove()

condition_05:  ⊢  

And then we rearrange a bit:

condition_06 = condition_05.left_add_both_sides(condition_05.lhs.operands[1].operand)

condition_06:  ⊢  

From an earlier condition, we can derive a bound on the rhs of condition_06 above:

condition_07 = condition_02.right_add_both_sides(one)

condition_07: ,  ⊢  

Then apply transitivity to obtain the following:

condition_08 = condition_06.apply_transitivity(condition_07)

condition_08: ,  ⊢  

We want to transform the $\text{mod}\;2^{t}$ on the lhs to the $\text{mod}\;1$ that we want in the eventual desired expression.
We can utilize the following theorem and subsequent instantiation to do that:

mod_abs_scaled

 ⊢  

from proveit import a, b, c
_a_sub, _b_sub, _c_sub = _two_pow_t, _thm_expr.lhs.operands[0], one
condition_equality_01 = mod_abs_scaled.instantiate({a: _a_sub, b: _b_sub, c: _c_sub})

condition_equality_01:  ⊢  

# clean up rhs side by distributing that factor of 2^t
condition_equality_02 = condition_equality_01.inner_expr().rhs.operands[0].distribute(1)

condition_equality_02:  ⊢  

Now we utilize that result, substituting the lhs for the rhs in our previous result:

condition_09 = condition_equality_02.sub_left_side_into(condition_08)

condition_09: ,  ⊢  

We can then divide both sides by the factor $2^{t}$ and simplify, and we are done:

condition_10 = condition_09.divide_both_sides(_two_pow_t)

condition_10: ,  ⊢  

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	163, 2, 3	,  ⊢
	: , : , :
2	instantiation	4, 255, 5, 99, 6, 7, 8*	,  ⊢
	: , : , :
3	instantiation	9, 77, 173, 133, 10*	⊢
	: , :
4	conjecture		⊢
	proveit.numbers.division.weak_div_from_numer_bound__pos_denom
5	instantiation	254, 255, 40	⊢
	: , :
6	instantiation	177, 11, 12	,  ⊢
	: , : , :
7	instantiation	13, 137	⊢
	:
8	instantiation	226, 14, 15	⊢
	: , : , :
9	conjecture		⊢
	proveit.numbers.division.div_as_mult
10	instantiation	226, 16, 17	⊢
	: , : , :
11	instantiation	46, 18, 19	,  ⊢
	: , : , :
12	instantiation	163, 20, 21	⊢
	: , : , :
13	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
14	instantiation	184, 101, 186, 22, 140*	⊢
	: , : , :
15	instantiation	203, 22	⊢
	:
16	instantiation	182, 23	⊢
	: , : , :
17	instantiation	24, 217, 25, 86, 42, 26*	⊢
	: , : , :
18	instantiation	27, 115, 28, 266, 29, 30*	⊢
	: , : , :
19	instantiation	31, 266, 115, 32, 33, 34*	,  ⊢
	: , : , :
20	instantiation	35, 255, 57, 266, 140*	⊢
	: , : , :
21	instantiation	36, 288, 239, 241, 173, 37, 38, 39*	⊢
	: , : , : , : , : , :
22	instantiation	286, 259, 40	⊢
	: , : , :
23	instantiation	41, 217, 260, 258, 42, 43*	⊢
	: , : , :
24	conjecture		⊢
	proveit.numbers.exponentiation.product_of_real_powers
25	instantiation	213, 260, 87	⊢
	: , :
26	instantiation	226, 44, 45	⊢
	: , : , :
27	conjecture		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
28	instantiation	213, 98, 97	⊢
	: , :
29	instantiation	46, 47, 48	⊢
	: , : , :
30	instantiation	226, 49, 50	⊢
	: , : , :
31	conjecture		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
32	instantiation	213, 99, 258	⊢
	: , :
33	instantiation	163, 51, 52	⊢
	: , : , :
34	instantiation	226, 53, 54	⊢
	: , : , :
35	conjecture		⊢
	proveit.numbers.modular.mod_abs_scaled
36	conjecture		⊢
	proveit.numbers.multiplication.distribute_through_subtract
37	instantiation	286, 259, 83	⊢
	: , : , :
38	instantiation	286, 259, 256	⊢
	: , : , :
39	instantiation	163, 55, 56	⊢
	: , : , :
40	instantiation	131, 57, 266, 58	⊢
	: , :
41	conjecture		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
42	instantiation	85, 248	⊢
	:
43	instantiation	59, 245, 244, 60*	⊢
	: , :
44	instantiation	238, 239, 283, 288, 241, 61, 245, 63, 62	⊢
	: , : , : , : , : , :
45	instantiation	243, 245, 63, 64	⊢
	: , : , :
46	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
47	instantiation	163, 65, 66, 67*	⊢
	: , : , :
48	instantiation	177, 68, 69	⊢
	: , : , :
49	instantiation	238, 288, 283, 239, 70, 241, 72, 73, 71	⊢
	: , : , : , : , : , :
50	instantiation	243, 72, 73, 74	⊢
	: , : , :
51	assumption		⊢
52	axiom		⊢
	proveit.physics.quantum.QPE._best_floor_def
53	instantiation	238, 239, 283, 288, 241, 75, 77, 242, 244	⊢
	: , : , : , : , : , :
54	instantiation	76, 244, 77, 246	⊢
	: , : , :
55	instantiation	163, 78, 79	⊢
	: , : , :
56	instantiation	122, 80, 81, 82	⊢
	: , : , : , :
57	instantiation	213, 83, 84	⊢
	: , :
58	instantiation	85, 250	⊢
	:
59	conjecture		⊢
	proveit.numbers.multiplication.mult_neg_right
60	instantiation	202, 245	⊢
	:
61	instantiation	257	⊢
	: , :
62	instantiation	286, 259, 86	⊢
	: , : , :
63	instantiation	286, 259, 87	⊢
	: , : , :
64	instantiation	261	⊢
	:
65	instantiation	88, 116, 132, 137, 89*	⊢
	: , : , :
66	instantiation	95, 146, 181	⊢
	: , :
67	instantiation	90, 91, 137, 92, 93*	⊢
	: , :
68	instantiation	110, 94	⊢
	: , :
69	instantiation	95, 96, 180	⊢
	: , :
70	instantiation	257	⊢
	: , :
71	instantiation	286, 259, 97	⊢
	: , : , :
72	instantiation	286, 259, 115	⊢
	: , : , :
73	instantiation	286, 259, 98	⊢
	: , : , :
74	instantiation	261	⊢
	:
75	instantiation	257	⊢
	: , :
76	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
77	instantiation	286, 259, 99	⊢
	: , : , :
78	instantiation	100, 244, 175, 101, 186	⊢
	: , : , : , : , :
79	instantiation	226, 102, 103	⊢
	: , : , :
80	instantiation	182, 104	⊢
	: , : , :
81	instantiation	182, 105	⊢
	: , : , :
82	instantiation	172, 175	⊢
	:
83	instantiation	106, 190, 255, 133	⊢
	: , :
84	instantiation	176, 256	⊢
	:
85	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
86	instantiation	176, 260	⊢
	:
87	instantiation	176, 107	⊢
	:
88	conjecture		⊢
	proveit.numbers.modular.mod_abs_of_difference_bound
89	instantiation	226, 108, 109	⊢
	: , : , :
90	conjecture		⊢
	proveit.numbers.modular.mod_abs_x_reduce_to_abs_x
91	instantiation	213, 193, 162	⊢
	: , :
92	instantiation	110, 111	⊢
	: , :
93	instantiation	112, 113, 114*	⊢
	:
94	instantiation	148, 265, 266, 209	⊢
	: , : , :
95	conjecture		⊢
	proveit.numbers.addition.commutation
96	instantiation	286, 259, 153	⊢
	: , : , :
97	instantiation	176, 115	⊢
	:
98	instantiation	131, 116, 255, 133	⊢
	: , :
99	instantiation	286, 272, 117	⊢
	: , : , :
100	conjecture		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
101	instantiation	286, 200, 118	⊢
	: , : , :
102	instantiation	182, 119	⊢
	: , : , :
103	instantiation	182, 120	⊢
	: , : , :
104	instantiation	203, 244	⊢
	:
105	instantiation	203, 175	⊢
	:
106	conjecture		⊢
	proveit.numbers.division.div_real_closure
107	instantiation	269, 270, 206	⊢
	: , : , :
108	instantiation	182, 121	⊢
	: , : , :
109	instantiation	122, 123, 124, 125	⊢
	: , : , : , :
110	conjecture		⊢
	proveit.numbers.ordering.relax_less
111	instantiation	126, 127, 128	⊢
	: , : , :
112	conjecture		⊢
	proveit.numbers.absolute_value.abs_neg_elim
113	instantiation	129, 130	⊢
	: , :
114	instantiation	141, 181, 180	⊢
	: , :
115	instantiation	131, 132, 255, 133	⊢
	: , :
116	instantiation	213, 190, 162	⊢
	: , :
117	instantiation	286, 134, 135	⊢
	: , : , :
118	instantiation	286, 136, 137	⊢
	: , : , :
119	instantiation	226, 138, 139	⊢
	: , : , :
120	instantiation	182, 140	⊢
	: , : , :
121	instantiation	141, 175, 181	⊢
	: , :
122	conjecture		⊢
	proveit.logic.equality.four_chain_transitivity
123	instantiation	238, 239, 283, 288, 241, 143, 175, 146, 142	⊢
	: , : , : , : , : , :
124	instantiation	238, 283, 239, 143, 144, 241, 175, 146, 161, 181	⊢
	: , : , : , : , : , :
125	instantiation	145, 239, 288, 241, 175, 146, 181, 147	⊢
	: , : , : , : , : , : , : , :
126	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
127	instantiation	148, 265, 266, 149	⊢
	: , : , :
128	instantiation	177, 150, 151	⊢
	: , : , :
129	conjecture		⊢
	proveit.numbers.addition.subtraction.nonpos_difference
130	instantiation	152, 237	⊢
	:
131	conjecture		⊢
	proveit.numbers.modular.mod_abs_real_closure
132	instantiation	213, 190, 153	⊢
	: , :
133	instantiation	154, 218, 155	⊢
	: , :
134	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational
135	instantiation	156, 218, 157	⊢
	: , :
136	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
137	instantiation	158, 195, 260	⊢
	: , :
138	instantiation	182, 159	⊢
	: , : , :
139	instantiation	203, 173	⊢
	:
140	instantiation	202, 173	⊢
	:
141	conjecture		⊢
	proveit.numbers.negation.distribute_neg_through_subtract
142	instantiation	160, 161, 181	⊢
	: , :
143	instantiation	257	⊢
	: , :
144	instantiation	257	⊢
	: , :
145	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
146	instantiation	286, 259, 162	⊢
	: , : , :
147	instantiation	261	⊢
	:
148	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
149	instantiation	163, 164, 165	⊢
	: , : , :
150	instantiation	166, 233	⊢
	:
151	instantiation	226, 167, 168	⊢
	: , : , :
152	conjecture		⊢
	proveit.numbers.rounding.floor_x_le_x
153	instantiation	176, 193	⊢
	:
154	conjecture		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
155	instantiation	286, 231, 169	⊢
	: , : , :
156	conjecture		⊢
	proveit.numbers.exponentiation.exp_rational_nonzero_closure
157	instantiation	262, 170, 171	⊢
	: , :
158	conjecture		⊢
	proveit.numbers.exponentiation.exp_real_pos_closure
159	instantiation	172, 173	⊢
	:
160	conjecture		⊢
	proveit.numbers.addition.add_complex_closure_bin
161	instantiation	174, 175	⊢
	:
162	instantiation	176, 237	⊢
	:
163	theorem		⊢
	proveit.logic.equality.sub_right_side_into
164	instantiation	177, 209, 178	⊢
	: , : , :
165	instantiation	179, 180, 181	⊢
	: , :
166	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
167	instantiation	182, 183	⊢
	: , : , :
168	instantiation	184, 185, 186, 204, 187*, 188*	⊢
	: , : , :
169	instantiation	286, 249, 285	⊢
	: , : , :
170	instantiation	286, 205, 285	⊢
	: , : , :
171	instantiation	281, 189	⊢
	:
172	conjecture		⊢
	proveit.numbers.multiplication.elim_one_left
173	instantiation	286, 259, 255	⊢
	: , : , :
174	conjecture		⊢
	proveit.numbers.negation.complex_closure
175	instantiation	286, 259, 190	⊢
	: , : , :
176	conjecture		⊢
	proveit.numbers.negation.real_closure
177	theorem		⊢
	proveit.logic.equality.sub_left_side_into
178	instantiation	191, 192	⊢
	:
179	conjecture		⊢
	proveit.numbers.absolute_value.abs_diff_reversal
180	instantiation	286, 259, 237	⊢
	: , : , :
181	instantiation	286, 259, 193	⊢
	: , : , :
182	axiom		⊢
	proveit.logic.equality.substitution
183	instantiation	194, 195, 260, 266, 196, 197, 198*	⊢
	: , : , : , :
184	conjecture		⊢
	proveit.numbers.division.frac_cancel_left
185	instantiation	286, 200, 199	⊢
	: , : , :
186	instantiation	286, 200, 201	⊢
	: , : , :
187	instantiation	202, 217	⊢
	:
188	instantiation	203, 204	⊢
	:
189	instantiation	286, 205, 206	⊢
	: , : , :
190	instantiation	286, 272, 207	⊢
	: , : , :
191	conjecture		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
192	instantiation	208, 265, 266, 209	⊢
	: , : , :
193	instantiation	286, 272, 210	⊢
	: , : , :
194	conjecture		⊢
	proveit.numbers.exponentiation.exp_factored_real
195	instantiation	286, 211, 212	⊢
	: , : , :
196	instantiation	213, 260, 258	⊢
	: , :
197	instantiation	214, 215	⊢
	: , :
198	instantiation	216, 217	⊢
	:
199	instantiation	286, 219, 218	⊢
	: , : , :
200	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
201	instantiation	286, 219, 220	⊢
	: , : , :
202	conjecture		⊢
	proveit.numbers.multiplication.elim_one_right
203	conjecture		⊢
	proveit.numbers.division.frac_one_denom
204	instantiation	286, 259, 221	⊢
	: , : , :
205	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
206	axiom		⊢
	proveit.physics.quantum.QPE._n_in_natural_pos
207	instantiation	286, 280, 222	⊢
	: , : , :
208	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
209	instantiation	223, 237	⊢
	:
210	instantiation	286, 280, 224	⊢
	: , : , :
211	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
212	instantiation	286, 225, 248	⊢
	: , : , :
213	conjecture		⊢
	proveit.numbers.addition.add_real_closure_bin
214	theorem		⊢
	proveit.logic.equality.equals_reversal
215	instantiation	226, 227, 228	⊢
	: , : , :
216	conjecture		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
217	instantiation	286, 259, 229	⊢
	: , : , :
218	instantiation	286, 231, 230	⊢
	: , : , :
219	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
220	instantiation	286, 231, 232	⊢
	: , : , :
221	instantiation	269, 270, 233	⊢
	: , : , :
222	instantiation	286, 234, 235	⊢
	: , : , :
223	conjecture		⊢
	proveit.numbers.rounding.real_minus_floor_interval
224	instantiation	236, 237	⊢
	:
225	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
226	axiom		⊢
	proveit.logic.equality.equals_transitivity
227	instantiation	238, 288, 283, 239, 240, 241, 244, 245, 242	⊢
	: , : , : , : , : , :
228	instantiation	243, 244, 245, 246	⊢
	: , : , :
229	instantiation	286, 272, 247	⊢
	: , : , :
230	instantiation	286, 249, 248	⊢
	: , : , :
231	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
232	instantiation	286, 249, 250	⊢
	: , : , :
233	conjecture		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
234	instantiation	251, 252, 253	⊢
	: , :
235	assumption		⊢
236	axiom		⊢
	proveit.numbers.rounding.floor_is_an_int
237	instantiation	254, 255, 256	⊢
	: , :
238	conjecture		⊢
	proveit.numbers.addition.disassociation
239	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
240	instantiation	257	⊢
	: , :
241	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
242	instantiation	286, 259, 258	⊢
	: , : , :
243	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
244	instantiation	286, 259, 266	⊢
	: , : , :
245	instantiation	286, 259, 260	⊢
	: , : , :
246	instantiation	261	⊢
	:
247	instantiation	286, 280, 278	⊢
	: , : , :
248	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
249	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
250	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
251	conjecture		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
252	conjecture		⊢
	proveit.numbers.number_sets.integers.zero_is_int
253	instantiation	262, 271, 274	⊢
	: , :
254	conjecture		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
255	instantiation	286, 272, 263	⊢
	: , : , :
256	instantiation	264, 265, 266, 267	⊢
	: , : , :
257	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
258	instantiation	286, 272, 268	⊢
	: , : , :
259	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
260	instantiation	269, 270, 285	⊢
	: , : , :
261	axiom		⊢
	proveit.logic.equality.equals_reflexivity
262	conjecture		⊢
	proveit.numbers.addition.add_int_closure_bin
263	instantiation	286, 280, 271	⊢
	: , : , :
264	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
265	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
266	instantiation	286, 272, 273	⊢
	: , : , :
267	axiom		⊢
	proveit.physics.quantum.QPE._phase_in_interval
268	instantiation	286, 280, 274	⊢
	: , : , :
269	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
270	instantiation	275, 276	⊢
	: , :
271	instantiation	277, 278, 279	⊢
	: , :
272	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
273	instantiation	286, 280, 282	⊢
	: , : , :
274	instantiation	281, 282	⊢
	:
275	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
276	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
277	conjecture		⊢
	proveit.numbers.exponentiation.exp_int_closure
278	instantiation	286, 287, 283	⊢
	: , : , :
279	instantiation	286, 284, 285	⊢
	: , : , :
280	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
281	conjecture		⊢
	proveit.numbers.negation.int_closure
282	instantiation	286, 287, 288	⊢
	: , : , :
283	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
284	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
285	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
286	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
287	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
288	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements