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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import k, l, m, n, t, defaults
from proveit.logic import InSet
from proveit.numbers import Mult
from proveit.physics.quantum.QPE import ( _m_domain, _t ) # QPE Common Expressions
from proveit.physics.quantum.QPE import (                 # QPE Axioms
    _alpha_m_def, _Psi_def )
from proveit.physics.quantum.QPE import (                 # QPE Theorems
    _phase_is_real, _psi_t_formula, _t_in_natural_pos )
from proveit.physics.quantum.QFT import invFT_on_matrix_elem

%proving _alpha_m_evaluation

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

defaults.assumptions = _alpha_m_evaluation.conditions

defaults.assumptions:

_alpha_m_def

 ⊢  

alpha_m_eq_01 = _alpha_m_def.instantiate()

alpha_m_eq_01:  ⊢  

_Psi_def

 ⊢  

alpha_m_eq_02 = _Psi_def.sub_right_side_into(alpha_m_eq_01)

alpha_m_eq_02:  ⊢  

_psi_t_formula

 ⊢  

# This instantiation requires we know that _t is in NaturalPos
psi_formula = _psi_t_formula.instantiate({t:_t})

psi_formula:  ⊢  

# Auto_simplification here pulls the constant coefficient
# out to the front of the bra-ket; for that auto-simplification
# factoring to work, however, we need the _phase_is_real theorem
# and the correct domain assumption for m.
alpha_m_eq_03 = psi_formula.sub_right_side_into(alpha_m_eq_02)

alpha_m_eq_03:  ⊢  

alpha_m_eq_04 = alpha_m_eq_03.inner_expr().rhs.operands[1].distribute(2)

alpha_m_eq_04:  ⊢  

# for convenience and clarity we name the summation domain
k_domain = psi_formula.rhs.operands[1].domain

k_domain:

invFT_on_matrix_elem

 ⊢  

matrix_elem = invFT_on_matrix_elem.instantiate(
    {n:_t, l:m}, assumptions=[InSet(k, k_domain), InSet(m, _m_domain)])

matrix_elem: ,  ⊢  

# We don't want to combine the two different exponentials through auto-simplification.
Mult.change_simplification_directives(combine_all_exponents=False)
alpha_m_eq_05 = (alpha_m_eq_04.inner_expr().rhs.operands[1]
               .summand.operands[1].substitute(matrix_elem))

alpha_m_eq_05:  ⊢  

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	331, 2, 3	⊢
	: , : , :
2	instantiation	4, 5, 6	⊢
	: , :
3	instantiation	7, 398, 8, 9, 10, 11	⊢
	: , : , : , :
4	theorem		⊢
	proveit.logic.equality.rhs_via_equality
5	instantiation	306, 12, 13	⊢
	: , : , :
6	instantiation	341, 14, 15*, 16*, 17*	⊢
	: , : , :
7	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
8	instantiation	338	⊢
	: , :
9	instantiation	338	⊢
	: , :
10	instantiation	107, 18	⊢
	: , :
11	instantiation	341, 19	⊢
	: , : , :
12	instantiation	306, 20, 21, 22*	⊢
	: , : , :
13	modus ponens	23, 152	⊢
14	modus ponens	24, 25	⊢
15	instantiation	101, 366	⊢
	: , :
16	instantiation	101, 366	⊢
	: , :
17	instantiation	331, 26, 27	⊢
	: , : , :
18	instantiation	196, 28, 29, 30	⊢
	: , : , : , :
19	modus ponens	31, 32	⊢
20	instantiation	306, 33, 34	⊢
	: , : , :
21	instantiation	35, 400	⊢
	:
22	instantiation	331, 36, 37	⊢
	: , : , :
23	instantiation	38, 390, 398, 322, 210, 323, 39*	⊢
	: , : , : , : , : , : , : , :
24	instantiation	140, 390	⊢
	: , : , : , : , : , : , :
25	generalization	40	⊢
26	instantiation	341, 41	⊢
	: , : , :
27	instantiation	331, 42, 43	⊢
	: , : , :
28	instantiation	315, 257, 227, 228, 44*	⊢
	: , :
29	instantiation	341, 45	⊢
	: , : , :
30	instantiation	107, 46	⊢
	: , :
31	instantiation	121, 390	⊢
	: , : , : , : , : , :
32	generalization	47	⊢
33	instantiation	48, 356	⊢
	:
34	axiom		⊢
	proveit.physics.quantum.QPE._Psi_def
35	conjecture		⊢
	proveit.physics.quantum.QPE._psi_t_formula
36	instantiation	341, 49	⊢
	: , : , :
37	instantiation	331, 50, 51	⊢
	: , : , :
38	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_distribution_over_summation
39	instantiation	331, 52, 53	⊢
	: , : , :
40	instantiation	54, 400, 366, 356, 55*	,  ⊢
	: , : , :
41	instantiation	331, 56, 57	⊢
	: , : , :
42	instantiation	321, 403, 398, 322, 58, 323, 241, 60	⊢
	: , : , : , : , : , :
43	instantiation	179, 322, 398, 403, 323, 59, 241, 60, 61*	⊢
	: , : , : , : , : , :
44	instantiation	331, 62, 63	⊢
	: , : , :
45	instantiation	107, 64	⊢
	: , :
46	instantiation	331, 65, 66	⊢
	: , : , :
47	instantiation	138, 67	⊢
	: , : , :
48	axiom		⊢
	proveit.physics.quantum.QPE._alpha_m_def
49	instantiation	196, 68, 69, 70	⊢
	: , : , : , :
50	instantiation	331, 71, 72	⊢
	: , : , :
51	instantiation	157, 158, 241, 73, 152, 74*	⊢
	: , : , :
52	instantiation	341, 75, 76*, 77*	⊢
	: , : , :
53	modus ponens	78, 79	⊢
54	conjecture		⊢
	proveit.physics.quantum.QFT.invFT_on_matrix_elem
55	instantiation	80, 226, 227, 228	,  ⊢
	: , :
56	instantiation	341, 81	⊢
	: , : , :
57	instantiation	331, 82, 83	⊢
	: , : , :
58	instantiation	338	⊢
	: , :
59	instantiation	338	⊢
	: , :
60	modus ponens	84, 143	⊢
61	instantiation	85, 241, 390, 86*, 87*	⊢
	: , : , :
62	instantiation	341, 88	⊢
	: , : , :
63	instantiation	290, 89	⊢
	:
64	instantiation	90, 202, 361, 91*	⊢
	: , :
65	instantiation	341, 92	⊢
	: , : , :
66	instantiation	184, 361, 93, 370, 316	⊢
	: , : , :
67	deduction	94	⊢
68	instantiation	155, 241, 403, 322, 323, 95	⊢
	: , : , : , : , : , :
69	instantiation	156, 403, 241, 95	⊢
	: , : , : , : , :
70	instantiation	157, 392, 241, 151, 95	⊢
	: , : , :
71	instantiation	331, 96, 97	⊢
	: , : , :
72	instantiation	156, 403, 398, 241, 151, 152	⊢
	: , : , : , : , :
73	instantiation	327	⊢
	: , : , :
74	instantiation	175, 241, 98	⊢
	: , :
75	modus ponens	99, 100	⊢
76	instantiation	101, 366	⊢
	: , :
77	instantiation	101, 366	⊢
	: , :
78	instantiation	102, 390	⊢
	: , : , : , :
79	generalization	103	⊢
80	conjecture		⊢
	proveit.numbers.division.neg_frac_neg_numerator
81	modus ponens	104, 105	⊢
82	instantiation	341, 106	⊢
	: , : , :
83	instantiation	107, 108	⊢
	: , :
84	instantiation	109	⊢
	: , : , :
85	conjecture		⊢
	proveit.numbers.exponentiation.product_of_posnat_powers
86	instantiation	360, 241	⊢
	:
87	conjecture		⊢
	proveit.numbers.numerals.decimals.add_1_1
88	instantiation	184, 361, 354, 232, 316, 110*	⊢
	: , : , :
89	instantiation	278, 361, 111	⊢
	: , :
90	conjecture		⊢
	proveit.numbers.multiplication.mult_neg_left
91	instantiation	196, 112, 113, 127	⊢
	: , : , : , :
92	instantiation	331, 114, 115	⊢
	: , : , :
93	instantiation	116, 221	⊢
	:
94	instantiation	343, 238, 181	,  ⊢
	: , :
95	instantiation	190, 261, 244, 187	⊢
	: , : , : , :
96	instantiation	155, 241, 403, 322, 323, 117	⊢
	: , : , : , : , : , :
97	instantiation	150, 398, 392, 322, 206, 151, 323, 118	⊢
	: , : , : , : , : , :
98	instantiation	280, 119, 172	⊢
	: , : , :
99	instantiation	140, 390	⊢
	: , : , : , : , : , : , :
100	generalization	120	⊢
101	conjecture		⊢
	proveit.core_expr_types.conditionals.satisfied_condition_reduction
102	axiom		⊢
	proveit.linear_algebra.addition.scalar_sum_extends_number_sum
103	instantiation	335, 238, 176	,  ⊢
	: , :
104	instantiation	121, 390	⊢
	: , :