In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit.logic import Equals, InSet
from proveit.numbers import Integer, Mult
from proveit.numbers.rounding import real_minus_floor_interval
from proveit.physics.quantum.QPE import (
_phase, _two_pow_t, _two_pow__t_minus_one)
from proveit.physics.quantum.QPE import (
_best_floor_def, _best_floor_is_in_m_domain, _delta_b_def, _phase_is_real, _t_in_natural_pos)
In [2]:
%proving _scaled_delta_b_floor_in_interval
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_scaled_delta_b_floor_in_interval:
(see dependencies)
_scaled_delta_b_floor_in_interval:
(see dependencies)
In [3]:
scaled_delta = _scaled_delta_b_floor_in_interval.operands[0]
scaled_delta: 
In [4]:
# interestingly, just importing this _delta_b_def can raise cascading
# side-effect errors and an eventual max recursion error unless
# we firt import some other seemingly unrelated items in the imports above
_delta_b_def
In [5]:
_best_floor_def
Elsewhere we have already established that $b_{f} \in \{0, \ldots, 2^t - 1\}$:
In [6]:
_best_floor_is_in_m_domain
In [7]:
from proveit import b
from proveit.physics.quantum.QPE import _b_floor
_delta_b_def_inst = _delta_b_def.instantiate({b: _b_floor})
_delta_b_def_inst: ⊢ 
In [8]:
eq_01 = _delta_b_def_inst.substitution(scaled_delta)
eq_01: ⊢ 
In [9]:
eq_02 = eq_01.inner_expr().rhs.distribute(1)
eq_02: ⊢ 
In [10]:
_best_floor_def_commuted = _best_floor_def.inner_expr().rhs.operands[0].commute()
_best_floor_def_commuted: ⊢ 
In [11]:
eq_03 = (eq_02.inner_expr().rhs.operands[1].
operand.substitute(_best_floor_def_commuted.rhs))
eq_03: ⊢ 
$(2^t\cdot\delta_{b_f})$ has now been expressed in the form $x - \lfloor x \rfloor$, and we have a theorem for the value of such an expression:
In [12]:
real_minus_floor_interval
To instantiate that theorem, we need to know that our argument $x = (2^t\cdot\varphi)$ is Real. In the imports in the top cell we have imported the _phase_is_real theorem and the _t_in_natural_pos axiom, which combined are sufficient for Prove-It to know that $(2^t\cdot\varphi)$ is Real:
In [13]:
_phase_is_real
In [14]:
_t_in_natural_pos
In [15]:
from proveit import x
interval_claim = real_minus_floor_interval.instantiate({x:Mult(_two_pow_t, _phase)})
interval_claim: ⊢ 
In [16]:
eq_04 = Equals(scaled_delta, interval_claim.element).prove()
eq_04: ⊢ 
In [17]:
eq_04.sub_left_side_into(interval_claim)
In [18]:
%qed
Out[18]:
