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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, c, k, m, r, x, y, defaults
from proveit.logic import InSet
from proveit.numbers import e, i, pi, Complex, Integer, Mod
from proveit.numbers.exponentiation import complex_power_of_complex_power, exp_eq
from proveit.numbers.modular import mod_natpos_in_interval
from proveit.numbers.number_sets.complex_numbers import exp_neg2pi_i_x
from proveit.physics.quantum.QPE import (
        _alpha_m_evaluation, _m_domain, _two_pow_t, _two_pow_t_is_nat_pos)

%proving _alpha_m_mod_evaluation

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

defaults.assumptions = _alpha_m_mod_evaluation.all_conditions()

defaults.assumptions:

_alpha_m_evaluation

 ⊢  

mod_natpos_in_interval

 ⊢  

_two_pow_t_is_nat_pos

 ⊢  

mod_natpos_in_interval.instantiate({a: m, b: _two_pow_t})

 ⊢  

_alpha_m_evaluation_inst = _alpha_m_evaluation.instantiate({m : Mod(m, _two_pow_t)})

_alpha_m_evaluation_inst:  ⊢  

exp_neg2pi_i_x

 ⊢  

# doesn't look like there is a way to insert the desired extra k factor
# during the instantiation (can the exp_neg2pi_i_x be better generalized?)
exp_neg2pi_i_x_inst = exp_neg2pi_i_x.instantiate({r: _two_pow_t, x: m})

exp_neg2pi_i_x_inst:  ⊢  

_m_domain

exp_eq

 ⊢  

exp_eq_inst = exp_eq.instantiate({a: k, x: exp_neg2pi_i_x_inst.lhs, y: exp_neg2pi_i_x_inst.rhs},
                  assumptions = [InSet(m, Integer), InSet(k, _m_domain)])

exp_eq_inst: ,  ⊢  

# what we have
exp_eq_inst.rhs.exponent.operand

# what we want
_alpha_m_evaluation_inst.rhs.operands[1].summand.operands[0].exponent.operand

exp_factored_k_01 = (
    _alpha_m_evaluation_inst.rhs.operands[1].summand.operands[0].exponent.inner_expr().
    operand.factorization(k, assumptions = [InSet(m, Integer), InSet(k, _m_domain)]))

exp_factored_k_01: ,  ⊢  

exp_factored_k_02 = exp_factored_k_01.inner_expr().rhs.operand.commute(0, 1)

exp_factored_k_02: ,  ⊢  

exp_factored_k_03 = exp_factored_k_02.sub_left_side_into(exp_eq_inst)

exp_factored_k_03: ,  ⊢  

exp_factored_k_04 = (
    _alpha_m_mod_evaluation.instance_expr.rhs.operands[1].summand.operands[0].exponent.inner_expr().
    operand.factorization(k, assumptions = [InSet(m, Integer), InSet(k, _m_domain)]))

exp_factored_k_04: ,  ⊢  

exp_factored_k_05 = exp_factored_k_04.inner_expr().rhs.operand.commute(0,1)

exp_factored_k_05: ,  ⊢  

exp_factored_k_06 = exp_factored_k_05.sub_left_side_into(exp_factored_k_03)

exp_factored_k_06: ,  ⊢  

# recall:
_alpha_m_evaluation_inst

 ⊢  

_alpha_m_evaluation_inst.inner_expr().rhs.operands[1].summand.factors[0].substitute(exp_factored_k_06)

 ⊢  

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4	⊢
	: , :
2	theorem		⊢
	proveit.logic.equality.rhs_via_equality
3	instantiation	5, 144	⊢
	:
4	instantiation	57, 6, 7*, 8*	⊢
	: , : , :
5	conjecture		⊢
	proveit.physics.quantum.QPE._alpha_m_evaluation
6	modus ponens	9, 10	⊢
7	instantiation	11, 135	⊢
	: , :
8	instantiation	11, 135	⊢
	: , :
9	instantiation	12, 127	⊢
	: , : , : , : , : , : , :
10	generalization	13	⊢
11	conjecture		⊢
	proveit.core_expr_types.conditionals.satisfied_condition_reduction
12	conjecture		⊢
	proveit.core_expr_types.lambda_maps.general_lambda_substitution
13	instantiation	16, 14, 15	,  ⊢
	: , : , :
14	instantiation	16, 17, 18	,  ⊢
	: , : , :
15	instantiation	82, 19, 20	,  ⊢
	: , : , :
16	theorem		⊢
	proveit.logic.equality.sub_left_side_into
17	instantiation	21, 89, 22, 23, 24, 25*, 26*	,  ⊢
	: , : , :
18	instantiation	82, 27, 28	,  ⊢
	: , : , :
19	instantiation	57, 29	,  ⊢
	: , : , :
20	instantiation	41, 89, 49	,  ⊢
	: , :
21	theorem		⊢
	proveit.numbers.exponentiation.exp_eq
22	instantiation	30, 31, 35	⊢
	: , :
23	instantiation	30, 31, 38	⊢
	: , :
24	instantiation	32, 121, 105, 33*, 34*	⊢
	: , :
25	instantiation	37, 54, 35, 89, 36*	,  ⊢
	: , : , :
26	instantiation	37, 54, 38, 89, 39*	,  ⊢
	: , : , :
27	instantiation	57, 40	,  ⊢
	: , : , :
28	instantiation	41, 89, 46	,  ⊢
	: , :
29	instantiation	98, 42, 43	,  ⊢
	: , : , :
30	conjecture		⊢
	proveit.numbers.exponentiation.exp_complex_closure
31	instantiation	158, 132, 44	⊢
	: , : , :
32	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.exp_neg2pi_i_x
33	instantiation	45, 68, 91, 56	⊢
	: , :
34	instantiation	45, 63, 91, 56	⊢
	: , :
35	instantiation	47, 46	⊢
	:
36	instantiation	48, 46, 89	,  ⊢
	: , :
37	conjecture		⊢
	proveit.numbers.exponentiation.complex_power_of_complex_power
38	instantiation	47, 49	⊢
	:
39	instantiation	48, 49, 89	,  ⊢
	: , :
40	instantiation	98, 50, 51	,  ⊢
	: , : , :
41	conjecture		⊢
	proveit.numbers.multiplication.commutation
42	instantiation	57, 52	,  ⊢
	: , : , :
43	instantiation	59, 53	,  ⊢
	: , :
44	instantiation	158, 138, 54	⊢
	: , : , :
45	conjecture		⊢
	proveit.numbers.division.neg_frac_neg_numerator
46	instantiation	55, 68, 91, 56	⊢
	: , :
47	conjecture		⊢
	proveit.numbers.negation.complex_closure
48	conjecture		⊢
	proveit.numbers.multiplication.mult_neg_left
49	instantiation	55, 63, 91, 56	⊢
	: , :
50	instantiation	57, 58	,  ⊢
	: , : , :
51	instantiation	59, 60	,  ⊢
	: , :
52	instantiation	98, 61, 62	,  ⊢
	: , : , :
53	instantiation	67, 89, 63, 69, 70, 71*, 72*	,  ⊢
	: , : , : , :
54	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
55	conjecture		⊢
	proveit.numbers.division.div_complex_closure
56	instantiation	64, 155	⊢
	:
57	axiom		⊢
	proveit.logic.equality.substitution
58	instantiation	98, 65, 66	,  ⊢
	: , : , :
59	theorem		⊢
	proveit.logic.equality.equals_reversal
60	instantiation	67, 89, 68, 69, 70, 71*, 72*	,  ⊢
	: , : , : , :
61	instantiation	76, 110, 77, 160, 111, 78, 123, 124, 114, 89, 107	,  ⊢
	: , : , : , : , : , : , :
62	instantiation	79, 160, 80, 110, 73, 111, 89, 123, 124, 114, 107	,  ⊢
	: , : , : , : , : , :
63	instantiation	82, 74, 75	⊢
	: , : , :
64	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
65	instantiation	76, 110, 77, 160, 111, 78, 123, 124, 114, 89, 115	,  ⊢
	: , : , : , : , : , : , :
66	instantiation	79, 160, 80, 110, 81, 111, 89, 123, 124, 114, 115	,  ⊢
	: , : , : , : , : , :
67	conjecture		⊢
	proveit.numbers.division.prod_of_fracs
68	instantiation	82, 83, 84	⊢
	: , : , :
69	instantiation	158, 86, 85	⊢
	: , : , :
70	instantiation	158, 86, 87	⊢
	: , : , :
71	instantiation	88, 89	⊢
	:
72	instantiation	90, 91	⊢
	:
73	instantiation	96	⊢
	: , : , : , :
74	instantiation	122, 108, 92	⊢
	: , :
75	instantiation	98, 93, 94	⊢
	: , : , :
76	conjecture		⊢
	proveit.numbers.multiplication.leftward_commutation
77	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3
78	instantiation	95	⊢
	: , : , :
79	conjecture		⊢
	proveit.numbers.multiplication.association
80	conjecture		⊢
	proveit.numbers.numerals.decimals.nat4
81	instantiation	96	⊢
	: , : , : , :
82	theorem		⊢
	proveit.logic.equality.sub_right_side_into
83	instantiation	122, 108, 97	⊢
	: , :
84	instantiation	98, 99, 100	⊢
	: , : , :
85	instantiation	158, 102, 101	⊢
	: , : , :
86	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
87	instantiation	158, 102, 103	⊢
	: , : , :
88	conjecture		⊢
	proveit.numbers.division.frac_one_denom
89	instantiation	158, 132, 104	⊢
	: , : , :
90	conjecture		⊢
	proveit.numbers.multiplication.elim_one_left
91	instantiation	158, 132, 105	⊢
	: , : , :
92	instantiation	122, 114, 107	⊢
	: , :
93	instantiation	109, 160, 145, 110, 106, 111, 108, 114, 107	⊢
	: , : , : , : , : , :
94	instantiation	109, 110, 145, 111, 112, 106, 123, 124, 114, 107	⊢
	: , : , : , : , : , :
95	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
96	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
97	instantiation	122, 114, 115	⊢
	: , :
98	axiom		⊢
	proveit.logic.equality.equals_transitivity
99	instantiation	109, 160, 145, 110, 113, 111, 108, 114, 115	⊢
	: , : , : , : , : , :
100	instantiation	109, 110, 145, 111, 112, 113, 123, 124, 114, 115	⊢
	: , : , : , : , : , :
101	instantiation	158, 117, 116	⊢
	: , : , :
102	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
103	instantiation	158, 117, 118	⊢
	: , : , :
104	instantiation	158, 136, 119	⊢
	: , : , :
105	instantiation	158, 136, 120	⊢
	: , : , :
106	instantiation	125	⊢
	: , :
107	instantiation	158, 132, 121	⊢
	: , : , :
108	instantiation	122, 123, 124	⊢
	: , :
109	conjecture		⊢
	proveit.numbers.multiplication.disassociation
110	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
111	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
112	instantiation	125	⊢
	: , :
113	instantiation	125	⊢
	: , :
114	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
115	instantiation	158, 132, 126	⊢
	: , : , :
116	instantiation	158, 128, 127	⊢
	: , : , :
117	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
118	instantiation	158, 128, 155	⊢
	: , : , :
119	instantiation	158, 141, 129	⊢
	: , : , :
120	instantiation	158, 141, 152	⊢
	: , : , :
121	instantiation	158, 136, 130	⊢
	: , : , :
122	conjecture		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
123	instantiation	158, 132, 131	⊢
	: , : , :
124	instantiation	158, 132, 133	⊢
	: , : , :
125	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
126	instantiation	158, 136, 134	⊢
	: , : , :
127	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
128	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
129	instantiation	158, 143, 135	⊢
	: , : , :
130	instantiation	158, 141, 150	⊢
	: , : , :
131	instantiation	158, 136, 137	⊢
	: , : , :
132	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
133	instantiation	158, 138, 139	⊢
	: , : , :
134	instantiation	158, 141, 140	⊢
	: , : , :
135	assumption		⊢
136	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
137	instantiation	158, 141, 142	⊢
	: , : , :
138	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
139	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
140	instantiation	158, 143, 144	⊢
	: , : , :
141	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
142	instantiation	158, 159, 145	⊢
	: , : , :
143	instantiation	146, 147, 148	⊢
	: , :
144	instantiation	149, 150, 155	⊢
	: , :
145	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
146	conjecture		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
147	conjecture		⊢
	proveit.numbers.number_sets.integers.zero_is_int
148	instantiation	151, 152, 153	⊢
	: , :
149	conjecture		⊢
	proveit.numbers.modular.mod_natpos_in_interval
150	assumption		⊢
151	conjecture		⊢
	proveit.numbers.addition.add_int_closure_bin
152	instantiation	158, 154, 155	⊢
	: , : , :
153	instantiation	156, 157	⊢
	:
154	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
155	conjecture		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
156	conjecture		⊢
	proveit.numbers.negation.int_closure
157	instantiation	158, 159, 160	⊢
	: , : , :
158	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
159	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
160	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements