# Proof of proveit.physics.quantum.QPE._best_floor_is_in_m_domain theorem¶

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit.physics.quantum.QPE import (
_b_floor,
_best_floor_def, _phase_in_interval, _phase_is_real, _two_pow_t_is_nat_pos)

In [2]:
%proving _best_floor_is_in_m_domain

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_best_floor_is_in_m_domain:
(see dependencies)
In [3]:
_best_floor_def

In [4]:
scaled_phase_floor = _best_floor_def.rhs

scaled_phase_floor:
In [5]:
scaled_phase = _best_floor_def.rhs.operand

scaled_phase:
In [6]:
from proveit.logic import InSet
from proveit.numbers import Integer
InSet(scaled_phase_floor, Integer).prove()

In [7]:
_phase_in_interval

In [8]:
_two_pow_t_is_nat_pos

In [9]:
_phase_upper_bound = _phase_in_interval.derive_element_upper_bound()

_phase_upper_bound:
In [10]:
_phase_lower_bound = _phase_in_interval.derive_element_lower_bound()

_phase_lower_bound:
In [11]:
scaled_phase_upper_bound = scaled_phase.deduce_bound([_phase_upper_bound])

scaled_phase_upper_bound:
In [12]:
scaled_phase_lower_bound = (
scaled_phase.deduce_bound(
[_phase_lower_bound.with_styles(direction='reversed')]))

scaled_phase_lower_bound:
In [13]:
scaled_phase_floor.deduce_bound([scaled_phase_upper_bound])

In [14]:
scaled_phase_floor.deduce_bound([scaled_phase_lower_bound])

In [15]:
%qed

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

Out[15]:
step typerequirementsstatement
0instantiation1, 2, 3
: , : , :
1theorem
proveit.logic.equality.sub_left_side_into
2instantiation4, 26, 5, 6, 7
: , : , :
3axiom
proveit.physics.quantum.QPE._best_floor_def
4conjecture
proveit.numbers.number_sets.integers.in_interval
5instantiation8, 52, 9
: , :
6instantiation10, 19
:
7instantiation11, 12, 13
: , :
8conjecture
9instantiation14, 46
:
10axiom
proveit.numbers.rounding.floor_is_an_int
11theorem
proveit.logic.booleans.conjunction.and_if_both
12instantiation15, 37, 19, 16, 17*
: , :
13instantiation18, 19, 52, 20
: , :
14conjecture
proveit.numbers.negation.int_closure
15conjecture
proveit.numbers.rounding.floor_increasing_less_eq
16instantiation21, 45, 37, 29, 22, 23, 24*
: , : , :
17instantiation25, 26
:
18conjecture
proveit.numbers.rounding.floor_of_real_below_int
19instantiation27, 45, 29
: , :
20instantiation28, 45, 29, 38, 30, 34, 31*
: , : , :
21conjecture
proveit.numbers.multiplication.weak_bound_via_right_factor_bound
22instantiation32, 37, 38, 39
: , : , :
23instantiation33, 34
: , :
24instantiation35, 41
:
25conjecture
proveit.numbers.rounding.floor_of_integer
26conjecture
proveit.numbers.number_sets.integers.zero_is_int
27conjecture
proveit.numbers.multiplication.mult_real_closure_bin
28conjecture
proveit.numbers.multiplication.strong_bound_via_right_factor_bound
29conjecture
proveit.physics.quantum.QPE._phase_is_real
30instantiation36, 37, 38, 39
: , : , :
31instantiation40, 41
:
32conjecture
proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
33conjecture
proveit.numbers.ordering.relax_less
34instantiation42, 55
:
35conjecture
proveit.numbers.multiplication.mult_zero_right
36conjecture
proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
37conjecture
proveit.numbers.number_sets.real_numbers.zero_is_real
38instantiation53, 47, 43
: , : , :
39axiom
proveit.physics.quantum.QPE._phase_in_interval
40conjecture
proveit.numbers.multiplication.elim_one_right
41instantiation53, 44, 45
: , : , :
42conjecture
proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
43instantiation53, 51, 46
: , : , :
44conjecture
proveit.numbers.number_sets.complex_numbers.real_within_complex
45instantiation53, 47, 48
: , : , :
46instantiation53, 49, 50
: , : , :
47conjecture
proveit.numbers.number_sets.real_numbers.rational_within_real
48instantiation53, 51, 52
: , : , :
49conjecture
proveit.numbers.number_sets.integers.nat_within_int
50theorem
proveit.numbers.numerals.decimals.nat1
51conjecture
proveit.numbers.number_sets.rational_numbers.int_within_rational
52instantiation53, 54, 55
: , : , :
53theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
54conjecture
proveit.numbers.number_sets.integers.nat_pos_within_int
55conjecture
proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
*equality replacement requirements