In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import l, defaults
from proveit.logic import Equals, InSet, Not, NotInSet
from proveit.numbers import Integer
from proveit.physics.quantum.QPE import _scaled_delta_b_is_zero_or_non_int
In [2]:
%proving _scaled_delta_b_not_eq_nonzeroInt
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_scaled_delta_b_not_eq_nonzeroInt:
(see dependencies)
_scaled_delta_b_not_eq_nonzeroInt:
(see dependencies)
In [3]:
defaults.assumptions = _scaled_delta_b_not_eq_nonzeroInt.conditions
defaults.assumptions: 
In [4]:
# for convenience, name the individual assumptions
ell_in_integers = defaults.assumptions[1]
ell_in_integers: 
In [5]:
# for convenience, name the individual assumptions
ell_not_zero = defaults.assumptions[2]
ell_not_zero: 
In [6]:
# for convenience, name the scaled delta expression
_scaled_delta = _scaled_delta_b_not_eq_nonzeroInt.instance_expr.lhs
_scaled_delta: 
In [7]:
_scaled_delta_b_is_zero_or_non_int
In [8]:
_scaled_delta_b_is_zero_or_non_int_inst = (
_scaled_delta_b_is_zero_or_non_int.instantiate())
_scaled_delta_b_is_zero_or_non_int_inst: 
⊢ 
⊢ 
In [9]:
# Assume to the contrary that _scaled_delta_b = ell
contradictory_assumption = Equals(_scaled_delta, l)
contradictory_assumption: 
In [10]:
# Need to explicitly include this, otherwise one of the final steps
# fails, with a generic, unhelpful error message.
contradictory_assumption.deduce_in_bool()
In [11]:
l_notin_ints_implies_not_l_in_ints = (
NotInSet(l, Integer).unfold(assumptions=[NotInSet(l, Integer)]).
as_implication(hypothesis=NotInSet(l, Integer)))
l_notin_ints_implies_not_l_in_ints: ⊢ 
In [12]:
# Must include this and previous cell; helps deal with a double negation later
l_notin_ints_implies_not_l_in_ints.contrapose()
In [13]:
contradictory_assumption_disjunction = (
contradictory_assumption.sub_right_side_into(
_scaled_delta_b_is_zero_or_non_int_inst,
assumptions=[*defaults.assumptions, contradictory_assumption]))
contradictory_assumption_disjunction: , ⊢ 
, ⊢ 
In [14]:
contradictory_assumption_gives_false = contradictory_assumption_disjunction.derive_contradiction()
contradictory_assumption_gives_false: , , , ⊢ 
, , , ⊢ 
In [15]:
contradictory_assumption_gives_false.as_implication(hypothesis=contradictory_assumption)
, , ⊢ 
In [16]:
%qed
Out[16]:
