Proof of proveit.physics.quantum.QPE.qpe_best_guarantee theorem

import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import defaults
from proveit import b, m
from proveit.logic import Or, Equals, InSet
from proveit.numbers import zero, one, Integer, Neg, Abs, Mod, sqrd
from proveit.numbers.number_sets.real_numbers import pi_between_3_and_4
from proveit.physics.quantum.QPE import (
    _outcome_prob, qpe_exact, _best_guarantee, _alpha_ideal_case, 
    _phase_is_real, _phase_in_interval,
    _b_round, _best_round_def, _best_round_is_int, _delta_b_round, _delta_b_def,
    _two_pow_t, _t_in_natural_pos, _two_pow_t_is_nat_pos)

%proving qpe_best_guarantee

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
qpe_best_guarantee:
(see dependencies)

_outcome_prob

 ⊢  

_best_guarantee

 ⊢  

Now instantiate _outcome_prob for the rounded, 'best' case

_m = _best_guarantee.lhs.base.operand.index

_m:

outcome_prob_bound = _outcome_prob.instantiate({m:_m}).apply_transitivity(_best_guarantee)

outcome_prob_bound:  ⊢  

Perform literal generalization, converting literals to quantified variables and their definining axioms into conditions

(outcome_prob_bound.generalize(
            qpe_best_guarantee.instance_param_lists(),
            conditions=qpe_best_guarantee.all_conditions())
       .inner_expr().instance_expr.instance_expr.instance_expr.with_wrapping()
       .inner_expr().instance_expr.instance_expr.with_wrapping())

 ⊢  

qpe_best_guarantee has been proven.  Now simply execute "%qed".

%qed

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

	step type	requirements	statement
0	literal generalization	1	⊢
1	instantiation	2, 3, 4	⊢
	: , : , :
2	theorem		⊢
	proveit.logic.equality.sub_left_side_into
3	conjecture		⊢
	proveit.physics.quantum.QPE._best_guarantee
4	instantiation	5, 6	⊢
	:
5	conjecture		⊢
	proveit.physics.quantum.QPE._outcome_prob
6	instantiation	7, 8, 16	⊢
	: , :
7	conjecture		⊢
	proveit.numbers.modular.mod_natpos_in_interval
8	instantiation	9, 10	⊢
	:
9	axiom		⊢
	proveit.numbers.rounding.round_is_an_int
10	instantiation	11, 12, 13	⊢
	: , :
11	conjecture		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
12	instantiation	14, 15, 16	⊢
	: , : , :
13	conjecture		⊢
	proveit.physics.quantum.QPE._phase_is_real
14	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
15	instantiation	17, 18	⊢
	: , :
16	conjecture		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
17	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
18	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real