In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, n, x, A, defaults
from proveit.logic import Equals, Forall, Implies, InSet, Not, NotEquals, Or, Set
from proveit.logic.booleans import unfold_is_bool
from proveit.numbers import (
zero, one, two, Add, Exp, frac, IntervalOO, Less, LessEq, Mult, Neg, Real)
from proveit.numbers.number_sets.real_numbers import not_int_if_not_int_in_interval
from proveit.physics.quantum.QPE import (
_b_floor, _b_round, _delta_b, _t,
_scaled_delta_b_floor_in_interval, _scaled_delta_b_round_in_interval)
In [2]:
%proving _scaled_delta_b_is_zero_or_non_int
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_scaled_delta_b_is_zero_or_non_int:
(see dependencies)
_scaled_delta_b_is_zero_or_non_int:
(see dependencies)
In [3]:
defaults.assumptions = _scaled_delta_b_is_zero_or_non_int.all_conditions()
defaults.assumptions: 
Deduce $2^t \delta_{b_f}$ in expanded interval $(-1, 1)$.¶
In [4]:
_scaled_delta_b_floor_in_interval
Perhaps because of the integer bounds involved, Prove-It has no trouble expanding that interval to the desired open interval $(-1, 1)$:
In [5]:
InSet(_scaled_delta_b_floor_in_interval.element, IntervalOO(Neg(one), one)).prove()
Deduce $2^t \delta_{b_r}$ in expanded interval $(-1, 1)$.¶
The automation is insufficient when trying to do the analogous thing for $2^t \delta_{b_r}$, so we have to do a bit more work. We need an explicit derivation of either $-1 < -\frac{1}{2}$ or $\frac{1}{2} < 1$ to allow the domain interval expansion.
In [6]:
_scaled_delta_b_round_in_interval
In [7]:
Less(frac(one, two), one).prove()
And from $\frac{1}{2}<1$, we can automatically derive $-1 < -\frac{1}{2}$.
Now Prove-It can derive the expanded interval membership for $2^t \delta_{b_r}$:
In [8]:
InSet(_scaled_delta_b_round_in_interval.element, IntervalOO(Neg(one), one)).prove()
Combine the results for both the $b_f$ and $b_r$ cases:¶
In [9]:
all_scaled_deltas_in_interval_neg_one_to_one = Forall(b,
InSet(Mult(Exp(two, _t), _delta_b), IntervalOO(Neg(one), one)),
domain=Set(_b_floor, _b_round)).prove()
all_scaled_deltas_in_interval_neg_one_to_one: ⊢ 
Establish that $(2^t \delta = 0) \lor (\lnot[2^t \delta = 0])$ using a version of the Law of the Excluded Middle¶
For convenience, we label the expression $2^{t}\delta_{b}$ as _scaled_delta:
In [10]:
_scaled_delta_b = all_scaled_deltas_in_interval_neg_one_to_one.instance_expr.element
_scaled_delta_b: 
In [11]:
# imported above
display(unfold_is_bool)
For convenience, we label our two mutually exclusive assumptions:
In [12]:
non_zero_assumption = NotEquals(_scaled_delta_b, zero)
non_zero_assumption: 
In [13]:
zero_assumption = Equals(_scaled_delta_b, zero)
zero_assumption: 
In [14]:
scaled_delta_b_is_zero_or_not = unfold_is_bool.instantiate({A: zero_assumption})
scaled_delta_b_is_zero_or_not: ⊢ 
Establish that the assumptions $(2^t \delta = 0)$ and $(\lnot[2^t \delta = 0])$ each imply that $(2^t \delta = 0) \lor (2^t \delta_{b} \notin \mathbb{Z})$¶
First, assuming that $2^t \delta_b \ne 0$¶
In [15]:
not_int_if_not_int_in_interval
In [16]:
not_zero_assumption_gives_not_int = not_int_if_not_int_in_interval.instantiate(
{n: zero, x: _scaled_delta_b},
assumptions=[*defaults.assumptions, non_zero_assumption])
not_zero_assumption_gives_not_int: 
, ⊢ 
, ⊢ 
In [17]:
Or(zero_assumption, not_zero_assumption_gives_not_int.expr).prove(
assumptions=[*defaults.assumptions, non_zero_assumption]).as_implication(hypothesis=non_zero_assumption)
In [18]:
not_zero_implies_not_eq_zero = non_zero_assumption.conclude_as_folded(
assumptions = [Not(zero_assumption)]).as_implication(hypothesis=Not(zero_assumption))
not_zero_implies_not_eq_zero: ⊢ 
In [19]:
Implies(Not(zero_assumption), Or(zero_assumption, not_zero_assumption_gives_not_int.expr)).prove()
Second, assuming that $2^t \delta_b = 0$¶
In [20]:
zero_assumption_gives_zero = zero_assumption.prove(assumptions=[*defaults.assumptions, zero_assumption])
zero_assumption_gives_zero: ⊢
⊢ In [21]:
Or(zero_assumption_gives_zero.expr, not_zero_assumption_gives_not_int.expr).prove(
assumptions=[*defaults.assumptions, zero_assumption]).as_implication(hypothesis=zero_assumption)
Thus in all cases we have the desired conclusion:¶
In [22]:
scaled_delta_b_is_zero_or_not.derive_via_singular_dilemma(_scaled_delta_b_is_zero_or_non_int.instance_expr)
In [23]:
%qed
Out[23]:
