In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit.logic import InSet
from proveit.numbers import Complex
from proveit.physics.quantum.QPE import (_alpha_m_def, _Psi_ket_is_normalized_vec,
_t_in_natural_pos, _two_pow_t_is_nat_pos)
In [2]:
%proving _alpha_are_complex
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_alpha_are_complex:
(see dependencies)
_alpha_are_complex:
(see dependencies)
In [3]:
defaults.assumptions = _alpha_are_complex.conditions
defaults.assumptions: 
In [4]:
_alpha_m_def
In [5]:
alpha_m_defined = _alpha_m_def.instantiate()
alpha_m_defined: 
⊢ 
⊢ 
In [6]:
_Psi_ket_is_normalized_vec
In [7]:
%qed
Out[7]:
