logo

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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, k, l, m, defaults
from proveit.logic import Forall, InSet, Set
from proveit.numbers import two, pi, i, Add, Integer, Mult, Exp
from proveit.physics.quantum.QPE import ModAdd
from proveit.physics.quantum.QPE import (
        _alpha_m_mod_as_geometric_sum,
        _b_floor, _best_floor_is_int, _non_int_delta_b_diff, _delta_b_is_real,
        _phase_from_best_with_delta_b, _phase_is_real, _t_in_natural_pos,
        _two_pow_t, _two_pow_t_is_nat_pos, _two_pow_t_minus_one_is_nat_pos)
In [2]:
%proving _alpha_summed
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_alpha_summed:
(see dependencies)
In [3]:
defaults.assumptions = _alpha_summed.all_conditions()
defaults.assumptions:

Disable reducing double exponents for now and keep a factor of $2$ from combining with $2^t$ in the steps below:

In [4]:
Exp.change_simplification_directives(reduce_double_exponent=False)
Exp.change_simplification_directives(factor_numeric_rational=True)
In [5]:
_t_in_natural_pos
 ⊢  
In [6]:
_two_pow_t_is_nat_pos
 ⊢  
In [7]:
_two_pow_t_minus_one_is_nat_pos
 ⊢  

To instantiate the _alpha_m_mod_as_geometric_sum theorem, we want $\ell \mapsto (b_f + \ell)$, but this requires that we establish that $(b_f+\ell) \in \mathbb{Z}$. This we accomplish by noting that $b_f$ is an integer.

In [8]:
_best_floor_is_int
 ⊢  
In [9]:
_alpha_m_mod_as_geometric_sum
 ⊢  
In [10]:
alpha_l_eq_01_alt = _alpha_m_mod_as_geometric_sum.instantiate({m: Add(_b_floor, l)})
alpha_l_eq_01_alt:  ⊢  

$(b+\ell)\,\text{mod}\,2^t$ is the definition of $b \oplus \ell$, so we can clean up the $\alpha$ subscript/indexing on the lhs:

In [11]:
b_modadd_l__def = ModAdd(_b_floor, l).definition()
b_modadd_l__def:  ⊢  
In [12]:
alpha_l_eq_02_alt = alpha_l_eq_01_alt.inner_expr().lhs.index.substitute(
    b_modadd_l__def.derive_reversed())
alpha_l_eq_02_alt:  ⊢  

Next we substitute in for the phase $\varphi$ in terms of $b$ and $\delta_{b}$.

In [13]:
_phase_from_best_with_delta_b
 ⊢  
In [14]:
_phase_from_best_with_delta_b_inst = _phase_from_best_with_delta_b.instantiate({b:_b_floor})
_phase_from_best_with_delta_b_inst:  ⊢  
In [15]:
# proactively recall _delta_b is real, so auto simplification will work
# as expected in the in next major step or two
_delta_b_is_real
 ⊢  
In [16]:
_delta_b_is_real.instantiate({b:_b_floor})
 ⊢  

Now we're ready to substitute back into our summation formula:

In [17]:
alpha_l_eq_03_alt = (
        alpha_l_eq_02_alt.inner_expr().rhs.factors[1].summand.
        base.exponent.factors[3].operands[0].
        substitute(_phase_from_best_with_delta_b_inst.rhs))
alpha_l_eq_03_alt:  ⊢  
In [18]:
alpha_l_eq_04_alt = (
        alpha_l_eq_03_alt.inner_expr().rhs.factors[1].summand.
        base.exponent.factors[3].operands[2].operand.distribute())
alpha_l_eq_04_alt:  ⊢  

We want to evaluate the summation as a finite geometric sum, but we need to establish that our exponential base $e^{2\pi i (\delta_{b} - \ell/{2^t})}$ is not equal to 1, which can be proven automatically given $\delta_{b} - \ell/{2^t} \notin \mathbb{Z}$.

In [19]:
_non_int_delta_b_diff
 ⊢  
In [20]:
_non_int_delta_b_diff.instantiate({b:_b_floor})
,  ⊢  

Now we're ready to evaluate the summation as a finite geometric sum, while we tweak the auto-simplification directives just a bit to keep things from being over-simplified:

In [21]:
# For this step, we re-enable the reduction of double exponentiation
# and disable combining exponents (to keep 2 and 2^t from combining into 2^{t+1}).
Exp.change_simplification_directives(reduce_double_exponent=True)
alpha_l_eq_05_alt = alpha_l_eq_04_alt.inner_expr().rhs.factors[1].geom_sum_reduce()
alpha_l_eq_05_alt: ,  ⊢  
In [22]:
alpha_l_eq_06_alt = (
        alpha_l_eq_05_alt.inner_expr().rhs.factors[1].numerator.operands[1].
        operand.exponent.distribute(3, right_factors=[_two_pow_t]))
alpha_l_eq_06_alt: ,  ⊢  
_alpha_summed may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [23]:
%qed

proveit.physics.quantum.QPE._alpha_summed has been proven.
Out[23]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation381, 2, 3,  ⊢  
  : , : , :
2instantiation329, 4, 5,  ⊢  
  : , : , :
3instantiation392, 6  ⊢  
  : , : , :
4instantiation329, 7, 8,  ⊢  
  : , : , :
5instantiation292, 286, 428, 321, 9, 10, 322, 401, 362, 193, 151, 242, 11*  ⊢  
  : , : , : , : , : , :
6instantiation392, 12  ⊢  
  : , : , :
7instantiation329, 13, 14, 15*  ⊢  
  : , : , :
8instantiation16, 37, 17, 18, 19, 20, 21*, 22*,  ⊢  
  : , : , : , :
9instantiation307  ⊢  
  : , : , :
10instantiation345  ⊢  
  : , :
11instantiation267, 321, 426, 322, 297, 207, 242, 23*  ⊢  
  : , : , : , : , : , :
12instantiation392, 24  ⊢  
  : , : , :
13instantiation329, 25, 26, 27*  ⊢  
  : , : , :
14instantiation28, 420, 29, 128, 324, 242, 233  ⊢  
  : , : , :
15instantiation381, 30, 31  ⊢  
  : , : , :
16conjecture  ⊢  
 proveit.numbers.summation.gen_finite_geom_sum
17instantiation303, 32, 33,  ⊢  
  : , : , :
18conjecture  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
19instantiation416, 34, 370  ⊢  
  : , :
20instantiation35, 36  ⊢  
  : , :
21instantiation361, 37  ⊢  
  :
22instantiation381, 38, 39  ⊢  
  : , : , :
23instantiation329, 40, 41  ⊢  
  : , : , :
24instantiation392, 42  ⊢  
  : , : , :
25instantiation303, 43, 44  ⊢  
  : , : , :
26instantiation45, 356  ⊢  
  :
27instantiation200, 321, 428, 426, 322, 70, 100, 297, 46  ⊢  
  : , : , : , : , : , :
28conjecture  ⊢  
 proveit.numbers.division.distribute_frac_through_sum
29instantiation345  ⊢  
  : , :
30instantiation392, 47  ⊢  
  : , : , :
31instantiation381, 48, 49  ⊢  
  : , : , :
32instantiation303, 50, 51,  ⊢  
  : , : , :
33instantiation392, 52  ⊢  
  : , : , :
34instantiation429, 430, 281  ⊢  
  : , : , :
35conjecture  ⊢  
 proveit.numbers.ordering.relax_less
36instantiation53, 54  ⊢  
  : , :
37instantiation312, 55, 58  ⊢  
  : , :
38instantiation392, 56  ⊢  
  : , : , :
39instantiation57, 116, 58, 242, 59*  ⊢  
  : , : , :
40instantiation329, 60, 61  ⊢  
  : , : , :
41instantiation332, 62, 63, 64  ⊢  
  : , : , : , :
42instantiation392, 65  ⊢  
  : , : , :
43instantiation66, 184  ⊢  
  :
44instantiation67, 356, 395  ⊢  
  : , :
45conjecture  ⊢  
 proveit.physics.quantum.QPE._phase_from_best_with_delta_b
46instantiation206, 68  ⊢  
  :
47instantiation69, 100, 207  ⊢  
  : , :
48instantiation200, 428, 321, 70, 71, 322, 100, 297, 72, 180  ⊢  
  : , : , : , : , : , :
49instantiation73, 321, 426, 322, 100, 297, 180, 74  ⊢  
  : , : , : , : , : , : , : , :
50instantiation75, 76, 77, 78*,  ⊢  
  :
51instantiation392, 79  ⊢  
  : , : , :
52instantiation381, 80, 81  ⊢  
  : , : , :
53conjecture  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
54instantiation82, 336, 107, 83, 84, 85*, 86*  ⊢  
  : , : , :
55instantiation429, 407, 87  ⊢  
  : , : , :
56instantiation381, 88, 89  ⊢  
  : , : , :
57conjecture  ⊢  
 proveit.numbers.exponentiation.complex_power_of_complex_power
58instantiation329, 90, 91  ⊢  
  : , : , :
59instantiation319, 321, 92, 426, 322, 93, 401, 362, 193, 151, 242  ⊢  
  : , : , : , : , : , :
60instantiation348, 324, 375, 349, 94  ⊢  
  : , : , : , : , :
61instantiation381, 95, 96  ⊢  
  : , : , :
62instantiation392, 97  ⊢  
  : , : , :
63instantiation392, 353  ⊢  
  : , : , :
64instantiation400, 324  ⊢  
  :
65instantiation392, 98  ⊢  
  : , : , :
66conjecture  ⊢  
 proveit.physics.quantum.QPE._alpha_m_mod_as_geometric_sum
67axiom  ⊢  
 proveit.physics.quantum.QPE._mod_add_def
68instantiation308, 99, 242, 233  ⊢  
  : , :
69conjecture  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
70instantiation345  ⊢  
  : , :
71instantiation345  ⊢  
  : , :
72instantiation206, 100  ⊢  
  :
73conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_general
74instantiation387  ⊢  
  :
75conjecture  ⊢  
 proveit.numbers.exponentiation.unit_complex_polar_num_neq_one
76instantiation329, 208, 187  ⊢  
  : , : , :
77instantiation303, 101, 102,  ⊢  
  : , : , :
78instantiation276, 103  ⊢  
  : , :
79instantiation392, 166  ⊢  
  : , : , :
80instantiation291, 428, 426, 321, 209, 322, 401, 362, 193, 151  ⊢  
  : , : , : , : , : , : , :
81instantiation392, 104  ⊢  
  : , : , :
82conjecture  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
83instantiation429, 414, 105  ⊢  
  : , : , :
84instantiation106, 107, 108, 386, 109, 110  ⊢  
  : , : , :
85instantiation381, 111, 112  ⊢  
  : , : , :
86instantiation332, 113, 114, 115  ⊢  
  : , : , : , :
87instantiation429, 388, 116  ⊢  
  : , : , :
88instantiation200, 321, 428, 426, 322, 117, 242, 313, 375  ⊢  
  : , : , : , : , : , :
89instantiation118, 375, 242, 376  ⊢  
  : , : , :
90instantiation285, 160, 119  ⊢  
  : , :
91instantiation381, 120, 121  ⊢  
  : , : , :
92conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat4
93instantiation122  ⊢  
  : , : , : , :
94instantiation429, 366, 123  ⊢  
  : , : , :
95instantiation392, 124  ⊢  
  : , : , :
96instantiation392, 125  ⊢  
  : , : , :
97instantiation394, 324  ⊢  
  :
98instantiation392, 126  ⊢  
  : , : , :
99instantiation429, 407, 127  ⊢  
  : , : , :
100instantiation308, 128, 242, 233  ⊢  
  : , :
101instantiation129, 130, 403, 131,  ⊢  
  : , :
102instantiation332, 132, 135, 133  ⊢  
  : , : , : , :
103instantiation392, 134  ⊢  
  : , : , :
104instantiation332, 163, 135, 136  ⊢  
  : , : , : , :
105instantiation429, 422, 137  ⊢  
  : , : , :
106conjecture  ⊢  
 proveit.numbers.ordering.less_eq_add_right_strong
107instantiation429, 414, 138  ⊢  
  : , : , :
108instantiation429, 388, 139  ⊢  
  : , : , :
109instantiation140, 408, 386, 141, 142, 143  ⊢  
  : , : , :
110conjecture  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
111instantiation392, 393  ⊢  
  : , : , :
112instantiation144, 375, 401, 145  ⊢  
  : , : , :
113instantiation381, 146, 147  ⊢  
  : , : , :
114instantiation381, 148, 149  ⊢  
  : , : , :
115instantiation387  ⊢  
  :
116conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
117instantiation345  ⊢  
  : , :
118conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_32
119instantiation285, 193, 151  ⊢  
  : , :
120instantiation319, 426, 428, 321, 150, 322, 160, 193, 151  ⊢  
  : , : , : , : , : , :
121instantiation319, 321, 428, 322, 209, 150, 401, 362, 193, 151  ⊢  
  : , : , : , : , : , :
122conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
123instantiation429, 379, 152  ⊢  
  : , : , :
124instantiation392, 178  ⊢  
  : , : , :
125instantiation381, 153, 154  ⊢  
  : , : , :
126instantiation276, 155  ⊢  
  : , :
127instantiation429, 414, 156  ⊢  
  : , : , :
128instantiation429, 407, 157  ⊢  
  : , : , :
129conjecture  ⊢  
 proveit.physics.quantum.QPE._non_int_delta_b_diff
130instantiation158, 321, 426, 322  ⊢  
  : , : , : , : , :
131assumption  ⊢  
132instantiation232, 159, 160, 161, 162*  ⊢  
  : , :
133instantiation276, 163  ⊢  
  : , :
134instantiation381, 164, 165  ⊢  
  : , : , :
135instantiation387  ⊢  
  :
136instantiation276, 166  ⊢  
  : , :
137instantiation429, 427, 167  ⊢  
  : , : , :
138instantiation429, 422, 168  ⊢  
  : , : , :
139instantiation429, 169, 170  ⊢  
  : , : , :
140conjecture  ⊢  
 proveit.numbers.multiplication.weak_bound_via_right_factor_bound
141instantiation346, 347, 431  ⊢  
  : , : , :
142instantiation171, 431  ⊢  
  :
143instantiation172, 428  ⊢  
  :
144conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add
145conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
146instantiation392, 173  ⊢  
  : , : , :
147instantiation381, 174, 175  ⊢  
  : , : , :
148instantiation392, 176  ⊢  
  : , : , :
149instantiation381, 177, 178  ⊢  
  : , : , :
150instantiation345  ⊢  
  : , :
151instantiation179, 297, 180  ⊢  
  : , :
152instantiation429, 411, 181  ⊢  
  : , : , :
153instantiation392, 182  ⊢  
  : ,