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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, x
from proveit.logic import Equals
from proveit.numbers import one, two, Add, frac, Neg
from proveit.numbers.rounding import (
    real_minus_floor_interval, round_in_terms_of_floor)
from proveit.physics.quantum.QPE import (
    _b_floor, _b_round, _best_round_def, _best_round_is_int,
    _delta_b_def, _phase_is_real, _t_in_natural_pos,
    _two_pow_t, _two_pow_t_is_nat_pos)

%proving _scaled_delta_b_round_in_interval

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

_scaled_delta = _scaled_delta_b_round_in_interval.operands[0]

_scaled_delta:

display(_delta_b_def)
display(_best_round_def)

 ⊢  

 ⊢  

_best_round_is_int

 ⊢  

_scaled_phase = _best_round_def.rhs.operand

_scaled_phase:

round_in_terms_of_floor

 ⊢  

round_in_terms_of_floor_inst = round_in_terms_of_floor.instantiate({x: _scaled_phase })

round_in_terms_of_floor_inst:  ⊢  

b_round_as_floor = round_in_terms_of_floor_inst.sub_right_side_into(_best_round_def)

b_round_as_floor:  ⊢  

_delta_b_def_inst = _delta_b_def.instantiate({b: _b_round})

_delta_b_def_inst:  ⊢  

eq_01 = _delta_b_def_inst.substitution(_scaled_delta)

eq_01:  ⊢  

eq_02 = eq_01.inner_expr().rhs.distribute(1)

eq_02:  ⊢  

b_round_as_floor

 ⊢  

eq_03 = (eq_02.inner_expr().rhs.operands[1].
         operand.substitute(b_round_as_floor.rhs))

eq_03:  ⊢  

desired_expr = Add(eq_03.rhs.operands[0], frac(one, two),
                   eq_03.rhs.operands[1], Neg(frac(one, two)))

desired_expr:

_scaled_delta_expr_manipulated = Equals(desired_expr, eq_03.rhs).prove()

_scaled_delta_expr_manipulated:  ⊢  

eq_04 = _scaled_delta_expr_manipulated.sub_left_side_into(eq_03)

eq_04:  ⊢  

real_minus_floor_interval

 ⊢  

diff_domain = real_minus_floor_interval.instantiate(
    {x : Add(eq_03.rhs.operands[0], frac(one, two))})

diff_domain:  ⊢  

diff_lower_bound = diff_domain.derive_element_lower_bound()

diff_lower_bound:  ⊢  

diff_upper_bound = diff_domain.derive_element_upper_bound()

diff_upper_bound:  ⊢  

# This works, but the auto_simplify=False is needed to keep the eq_04.rhs expression
# from being simplified (by canceling the introduced ±1/2 terms)
upper_bound = (
    eq_04.rhs.bound_via_term_bound(diff_upper_bound, auto_simplify=False).
    inner_expr().rhs.simplify())

upper_bound:  ⊢  

upper_bound.inner_expr().lhs.substitute(eq_04)

 ⊢  

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

%qed

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

	step type	requirements	statement
0	instantiation	1, 2, 3, 4, 5	⊢
	: , : , :
1	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalCO
2	reference	20	⊢
3	reference	120	⊢
4	instantiation	12, 6, 41	⊢
	: , : , :
5	instantiation	7, 8, 9	⊢
	: , :
6	instantiation	129, 157, 10	⊢
	: , :
7	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
8	instantiation	12, 11, 14	⊢
	: , : , :
9	instantiation	12, 13, 14	⊢
	: , : , :
10	instantiation	118, 130, 15	⊢
	: , :
11	instantiation	16, 20, 33, 21, 17, 18*, 23*	⊢
	: , : , :
12	theorem		⊢
	proveit.logic.equality.sub_left_side_into
13	instantiation	19, 20, 21, 132, 22, 23*, 24*	⊢
	: , : , :
14	instantiation	92, 25, 26	⊢
	: , : , :
15	instantiation	30, 82	⊢
	:
16	conjecture		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
17	instantiation	27, 33, 132, 34	⊢
	: , : , :
18	instantiation	92, 28, 29	⊢
	: , : , :
19	conjecture		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
20	instantiation	30, 120	⊢
	:
21	instantiation	31, 33, 132, 34	⊢
	: , : , :
22	instantiation	32, 33, 132, 34	⊢
	: , : , :
23	instantiation	124, 35, 36	⊢
	: , : , :
24	instantiation	37, 153, 38, 155, 106*, 39*, 40*	⊢
	: , : , : , :
25	instantiation	92, 41, 42	⊢
	: , : , :
26	instantiation	92, 43, 44	⊢
	: , : , :
27	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
28	instantiation	45, 52	⊢
	:
29	instantiation	46, 52, 47	⊢
	: , :
30	conjecture		⊢
	proveit.numbers.negation.real_closure
31	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
32	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
33	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
34	instantiation	48, 110, 49*	⊢
	:
35	instantiation	65, 66, 50, 158, 67, 51, 69, 72, 70, 52	⊢
	: , : , : , : , : , :
36	instantiation	53, 158, 66, 67, 69, 72, 70, 54	⊢
	: , : , : , : , : , : , : , :
37	conjecture		⊢
	proveit.numbers.addition.rational_pair_addition
38	instantiation	55, 153	⊢
	:
39	instantiation	56, 116, 88, 134	⊢
	: , :
40	instantiation	124, 57, 58	⊢
	: , : , :
41	instantiation	138, 59	⊢
	: , : , :
42	instantiation	60, 158, 66, 67, 151, 61, 62, 63*	⊢
	: , : , : , : , : , :
43	axiom		⊢
	proveit.physics.quantum.QPE._best_round_def
44	instantiation	64, 119	⊢
	:
45	conjecture		⊢
	proveit.numbers.addition.elim_zero_right
46	conjecture		⊢
	proveit.numbers.addition.commutation
47	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
48	conjecture		⊢
	proveit.numbers.rounding.real_minus_floor_interval
49	instantiation	65, 66, 161, 158, 67, 68, 69, 72, 70	⊢
	: , : , : , : , : , :
50	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3
51	instantiation	71	⊢
	: , : , :
52	instantiation	85, 72	⊢
	:
53	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
54	instantiation	73	⊢
	:
55	conjecture		⊢
	proveit.numbers.negation.int_closure
56	conjecture		⊢
	proveit.numbers.division.neg_frac_neg_numerator
57	instantiation	74, 161, 75, 76, 77, 78	⊢
	: , : , : , :
58	instantiation	79, 116, 88, 80	⊢
	: , : , :
59	instantiation	81, 152	⊢
	:
60	conjecture		⊢
	proveit.numbers.multiplication.distribute_through_subtract
61	instantiation	159, 156, 130	⊢
	: , : , :
62	instantiation	159, 156, 82	⊢
	: , : , :
63	instantiation	92, 83, 84	⊢
	: , : , :
64	conjecture		⊢
	proveit.numbers.rounding.round_in_terms_of_floor
65	conjecture		⊢
	proveit.numbers.addition.disassociation
66	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
67	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
68	instantiation	87	⊢
	: , :
69	instantiation	159, 156, 119	⊢
	: , : , :
70	instantiation	85, 86	⊢
	:
71	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
72	instantiation	159, 156, 120	⊢
	: , : , :
73	axiom		⊢
	proveit.logic.equality.equals_reflexivity
74	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
75	instantiation	87	⊢
	: , :
76	instantiation	87	⊢
	: , :
77	instantiation	150, 88	⊢
	:
78	instantiation	89, 116, 90*	⊢
	: , :
79	conjecture		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
80	conjecture		⊢
	proveit.numbers.numerals.decimals.add_1_1
81	axiom		⊢
	proveit.physics.quantum.QPE._delta_b_def
82	instantiation	131, 128, 157, 91	⊢
	: , :
83	instantiation	92, 93, 94	⊢
	: , : , :
84	instantiation	95, 96, 97, 98	⊢
	: , : , : , :
85	conjecture		⊢
	proveit.numbers.negation.complex_closure
86	instantiation	162, 99, 100	⊢
	: , : , :
87	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
88	instantiation	159, 156, 133	⊢
	: , : , :
89	conjecture		⊢
	proveit.numbers.multiplication.mult_neg_right
90	instantiation	141, 116	⊢
	:
91	instantiation	146, 164	⊢
	:
92	theorem		⊢
	proveit.logic.equality.sub_right_side_into
93	instantiation	101, 116, 117, 102, 103	⊢
	: , : , : , : , :
94	instantiation	124, 104, 105	⊢
	: , : , :
95	conjecture		⊢
	proveit.logic.equality.four_chain_transitivity
96	instantiation	138, 106	⊢
	: , : , :
97	instantiation	138, 107	⊢
	: , : , :
98	instantiation	150, 117	⊢
	:
99	instantiation	165, 108	⊢
	: , :
100	instantiation	109, 110	⊢
	:
101	conjecture		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
102	instantiation	159, 112, 111	⊢
	: , : , :
103	instantiation	159, 112, 113	⊢
	: , : , :
104	instantiation	138, 114	⊢
	: , : , :
105	instantiation	138, 115	⊢
	: , : , :
106	instantiation	140, 116	⊢
	:
107	instantiation	140, 117	⊢
	:
108	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.int_within_complex
109	axiom		⊢
	proveit.numbers.rounding.floor_is_an_int
110	instantiation	118, 119, 120	⊢
	: , :
111	instantiation	159, 122, 121	⊢
	: , : , :
112	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
113	instantiation	159, 122, 123	⊢
	: , : , :
114	instantiation	124, 125, 126	⊢
	: , : , :
115	instantiation	138, 127	⊢
	: , : , :
116	instantiation	159, 156, 132	⊢
	: , : , :
117	instantiation	159, 156, 128	⊢
	: , : , :
118	conjecture		⊢
	proveit.numbers.addition.add_real_closure_bin
119	instantiation	129, 157, 130	⊢
	: , :
120	instantiation	131, 132, 133, 134	⊢
	: , :
121	instantiation	159, 136, 135	⊢
	: , : , :
122	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
123	instantiation	159, 136, 137	⊢
	: , : , :
124	axiom		⊢
	proveit.logic.equality.equals_transitivity
125	instantiation	138, 139	⊢
	: , : , :
126	instantiation	140, 151	⊢
	:
127	instantiation	141, 151	⊢
	:
128	instantiation	159, 144, 142	⊢
	: , : , :
129	conjecture		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
130	conjecture		⊢
	proveit.physics.quantum.QPE._phase_is_real
131	conjecture		⊢
	proveit.numbers.division.div_real_closure
132	instantiation	159, 144, 143	⊢
	: , : , :
133	instantiation	159, 144, 145	⊢
	: , : , :
134	instantiation	146, 147	⊢
	:
135	instantiation	159, 148, 164	⊢
	: , : , :
136	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
137	instantiation	159, 148, 149	⊢
	: , : , :
138	axiom		⊢
	proveit.logic.equality.substitution
139	instantiation	150, 151	⊢
	:
140	conjecture		⊢
	proveit.numbers.division.frac_one_denom
141	conjecture		⊢
	proveit.numbers.multiplication.elim_one_right
142	instantiation	159, 154, 152	⊢
	: , : , :
143	instantiation	159, 154, 153	⊢
	: , : , :
144	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
145	instantiation	159, 154, 155	⊢
	: , : , :
146	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
147	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
148	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
149	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
150	conjecture		⊢
	proveit.numbers.multiplication.elim_one_left
151	instantiation	159, 156, 157	⊢
	: , : , :
152	conjecture		⊢
	proveit.physics.quantum.QPE._best_round_is_int
153	instantiation	159, 160, 158	⊢
	: , : , :
154	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
155	instantiation	159, 160, 161	⊢
	: , : , :
156	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
157	instantiation	162, 163, 164	⊢
	: , : , :
158	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
159	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
160	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
161	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
162	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
163	instantiation	165, 166	⊢
	: , :
164	conjecture		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
165	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
166	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements