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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, e, l, x, y, defaults
from proveit.logic import Iff, InSet, Or, SubsetEq, Union
from proveit.numbers import zero, Add, subtract, greater_eq, Less, Neg, NaturalPos
from proveit.numbers.ordering import less_or_greater_eq
from proveit.physics.quantum.QPE import (
_full_domain, _modabs_in_full_domain_simp, _neg_domain, _pos_domain)
from proveit.physics.quantum.QPE import (
_two_pow_t, _two_pow_t__minus_one, _t_in_natural_pos, _two_pow_t_minus_one_is_nat_pos)

In [2]:
%proving _fail_sum_prob_conds_equiv_lemma

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

defaults.assumptions:

We want to derive the logical equivalence (if and only if) between the following conditions:

In [4]:
lhs_condition = _fail_sum_prob_conds_equiv_lemma.instance_expr.instance_expr.lhs

lhs_condition:
In [5]:
rhs_condition = _fail_sum_prob_conds_equiv_lemma.instance_expr.instance_expr.rhs

rhs_condition:

(1) $\text{lhs} \Rightarrow \text{rhs}$. This direction is straightforward using the fact that $\{-2^{t-1}+1~\ldotp \ldotp~-(e+1)\} \cup \{e + 1~\ldotp \ldotp~2^{t-1}\} \subseteq \{-2^{t-1}+1~\ldotp \ldotp~2^{t-2}\}$.

In [6]:
SubsetEq(Union(_neg_domain, _pos_domain), _full_domain).prove()

In [7]:
rhs_condition.prove(assumptions=defaults.assumptions + (lhs_condition,))


(2) $\text{lhs} \Leftarrow \text{rhs}$.

Going from rhs to lhs requires us to consider the non-negative/negative cases separately.

2(a): $\text{lhs} \Leftarrow \text{rhs}$. The NON-NEGATIVE case.

In [8]:
# update our default assumptions
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions() + [rhs_condition, greater_eq(l, zero)]

defaults.assumptions:
In [9]:
_modabs_in_full_domain_simp

In [10]:
_modabs_in_full_domain_simp.instantiate().sub_right_side_into(rhs_condition.operands[1])

In [11]:
InSet(subtract(l, e), NaturalPos).prove()

, ,  ⊢
In [12]:
lhs_condition.prove()

, ,  ⊢

2(b): $\text{lhs} \Leftarrow \text{rhs}$. The NEGATIVE case.

In [13]:
# update our default assumptions
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions() + [rhs_condition, Less(l, zero)]

defaults.assumptions:
In [14]:
_modabs_in_full_domain_simp.instantiate().sub_right_side_into(rhs_condition.operands[1])

In [15]:
InSet(Neg(Add(e, l)), NaturalPos).prove()

, ,  ⊢
In [16]:
lhs_condition.prove()

, ,  ⊢

Since either $l \geq 0$ or $l < 0$ but we can derive lhs_condition either way, then lhs_condition must be true (under these assumptions).

In [17]:
# update our default assumptions (removing the specifics about ell being negative or non-negative)
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions() + [rhs_condition]

defaults.assumptions:
In [18]:
less_or_greater_eq

In [19]:
less_or_greater_eq.instantiate({x:l, y:zero})

In [20]:
Or(Less(l, zero), greater_eq(l, zero)).derive_via_dilemma(lhs_condition)

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

In [21]:
%qed

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

Out[21]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4
: , :
2theorem
proveit.logic.booleans.implication.iff_intro
3deduction5
4deduction6
5instantiation85, 7, 8,  ⊢
: , :
6instantiation9, 10, 11, 26, 12, 13,  ⊢
: , : , :
7instantiation365, 14, 15,  ⊢
: , : , :
8instantiation283, 24
: , :
9theorem
proveit.logic.booleans.disjunction.singular_constructive_dilemma
10instantiation16, 18
: , :
11instantiation17, 18
: , :
12deduction19,  ⊢
13deduction20,  ⊢
14instantiation21, 394, 35, 22, 23
: , : , :
15instantiation378, 24
: , :
16axiom
proveit.logic.booleans.disjunction.left_in_bool
17axiom
proveit.logic.booleans.disjunction.right_in_bool
18instantiation25, 26
:
19instantiation85, 27, 260, ,  ⊢
: , :
20instantiation85, 28, 260, ,  ⊢
: , :
21conjecture
proveit.logic.sets.unification.union_inclusion
22instantiation30, 377, 83, 404, 29
: , : , : , :
23instantiation30, 377, 113, 404, 31
: , : , : , :
24assumption
25conjecture
proveit.logic.booleans.in_bool_if_true
26instantiation32, 328, 132
: , :
27instantiation34, 394, 35, 33, ,  ⊢
: , : , :
28instantiation34, 394, 35, 36, ,  ⊢
: , : , :
29instantiation40, 319, 37, 38, 52, 39
: , :
30conjecture
proveit.numbers.number_sets.integers.interval_subset_eq
31instantiation40, 319, 41, 42, 43, 44
: , :
32conjecture
proveit.numbers.ordering.less_or_greater_eq
33instantiation110, 45, 46, ,  ⊢
: , :
34conjecture
proveit.logic.sets.unification.membership_folding
35instantiation323
: , :
36instantiation114, 47, 48, ,  ⊢
: , :
37instantiation335
: , : , :
38instantiation57, 154, 49
: , :
39instantiation325, 50
: , :
40conjecture
proveit.logic.booleans.conjunction.and_if_all
41instantiation335
: , : , :
42instantiation51, 52, 53
: , : , :
43instantiation131, 384, 351, 54, 55, 56*
: , : , :
44instantiation57, 151, 58
: , :
45instantiation63, 377, 83, 352, 59, ,  ⊢
: , : , :
46instantiation61, 60, ,  ⊢
: , :
47instantiation61, 62, ,  ⊢
: , :
48instantiation63, 113, 404, 352, 64, ,  ⊢
: , : , :
49instantiation303
:
50instantiation149, 156, 65
: , : , :
51conjecture
proveit.numbers.ordering.transitivity_less_eq_less_eq
52instantiation131, 66, 351, 75, 76, 67*, 68*
: , : , :
53instantiation131, 172, 69, 70, 71, 72*, 73*
: , : , :
54instantiation327, 75, 384
: , :
55instantiation74, 351, 75, 384, 76, 77
: , : , :
56instantiation314, 78, 277, 79
: , : , : , :
57conjecture
proveit.numbers.ordering.relax_equal_to_less_eq
58instantiation303
:
59instantiation85, 155, 80, ,  ⊢
: , :
60instantiation82, 113, 404, 352, 81, ,  ⊢
: , : , :
61theorem
proveit.logic.sets.membership.unfold_not_in_set
62instantiation82, 377, 83, 352, 84, ,  ⊢
: , : , :
63conjecture
proveit.numbers.number_sets.integers.in_interval
64instantiation85, 86, 152, ,  ⊢
: , :
65instantiation187, 409
:
66instantiation87, 319, 88, 89, 384, 206
: , :
67instantiation314, 90, 91, 92
: , : , : , :
68instantiation331, 93
: , :
69instantiation229, 397, 132
: , :
70instantiation327, 207, 397
: , :
71instantiation94, 95, 96, 411, 97, 98
: , : , :
72instantiation331, 99
: , :
73instantiation314, 100, 101, 102
: , : , : , :
74conjecture
75instantiation412, 401, 103
: , : , :
76instantiation188, 400, 399, 391
: , : , :
77instantiation166, 406
:
78instantiation272, 104, 105
: , : , :
79instantiation331, 297
: , :
80instantiation131, 309, 384, 106, 107, 108*, 109*, ,  ⊢
: , : , :
81instantiation110, 111, 112, ,  ⊢
: , :
82conjecture
proveit.numbers.number_sets.integers.int_not_in_interval
83instantiation410, 113
:
84instantiation114, 115, 116, ,  ⊢
: , :
85theorem
proveit.logic.booleans.conjunction.and_if_both
86instantiation131, 351, 384, 117, 118, 119*, 120*, ,  ⊢
: , : , :
87conjecture
88instantiation335
: , : , :
89instantiation412, 401, 121
: , : , :
90instantiation272, 122, 123
: , : , :
91instantiation303
:
92instantiation331, 124
: , :
93instantiation314, 184, 125, 126
: , : , : , :
94conjecture
95instantiation412, 413, 127
: , : , :
96instantiation412, 413, 128
: , : , :
97instantiation129, 397, 132, 351, 294, 130
: , : , :
98instantiation131, 344, 132, 203, 133, 134*, 135*
: , : , :
99instantiation314, 184, 185, 136
: , : , : , :
100instantiation299, 300, 414, 406, 302, 138, 175, 387, 137
: , : , : , : , : , :
101instantiation299, 414, 300, 138, 254, 302, 175, 387, 322, 342
: , : , : , : , : , :
102instantiation314, 139, 140, 141
: , : , : , :
103instantiation412, 407, 399
: , : , :
104instantiation333, 142
: , : , :
105instantiation272, 143, 144
: , : , :
106instantiation365, 366, 145, ,  ⊢
: , : , :
107instantiation157, 145, ,  ⊢
:
108instantiation272, 146, 147
: , : , :
109instantiation331, 148,  ⊢
: , :
110theorem
proveit.logic.booleans.disjunction.or_if_only_left
111instantiation149, 326, 150,  ⊢
: , : , :
112instantiation153, 328, 151, 152
: , :
113instantiation403, 376, 400
: , :
114theorem
proveit.logic.booleans.disjunction.or_if_only_right
115instantiation153, 154, 328, 155
: , :
116instantiation311, 156, 296,  ⊢
: , : , :
117instantiation327, 328, 206,  ⊢
: , :
118instantiation157, 158, ,  ⊢
:
119instantiation340, 370, 337
: , :
120instantiation272, 159, 160,  ⊢
: , : , :
121instantiation412, 407, 392
: , : , :
122instantiation333, 244
: , : , :
123instantiation272, 161, 162
: , : , :
124instantiation333, 271
: , : , :
125instantiation340, 322, 342
: , :
126instantiation331, 163
: , :
127instantiation164, 414, 300
: , :
128instantiation164, 414, 165
: , :
129conjecture
proveit.numbers.multiplication.strong_bound_via_right_factor_bound
130instantiation187, 394
:
131conjecture
132conjecture
proveit.numbers.number_sets.real_numbers.zero_is_real
133instantiation166, 319
:
134instantiation278, 167, 168
: , : , :
135instantiation282, 387, 370, 169, 170
: , : , :
136instantiation331, 171
: , :
137instantiation412, 396, 172
: , : , :
138instantiation323
: , :
139instantiation173, 406, 175, 387, 322, 342
: , : , : , : , : , : , :
140instantiation247, 300, 414, 302, 174, 257, 175, 322, 387, 342, 176*
: , : , : , : , : , :
141instantiation247, 406, 414, 300, 257, 302, 337, 387, 342, 258*
: , : , : , : , : , :
142instantiation272, 177, 178
: , : , :
143instantiation299, 300, 414, 406, 302, 179, 336, 342, 370
: , : , : , : , : , :
144instantiation195, 370, 336, 183
: , : , :
145instantiation180, 181, ,  ⊢
:
146instantiation299, 406, 414, 300, 289, 302, 370, 292, 342
: , : , : , : , : , :
147instantiation182, 370, 292, 183
: , : , :
148instantiation314, 184, 185, 186,  ⊢
: , : , : , :
149axiom
proveit.numbers.ordering.transitivity_less_less
150instantiation187, 217
:
151instantiation365, 366, 409
: , : , :
152instantiation188, 377, 404, 364
: ,