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

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

from proveit import defaults, Lambda
from proveit import a, b, t
from proveit.logic import Exists, Equals
from proveit.numbers import NaturalPos
from proveit.physics.quantum.QPE import _precision_guarantee

%proving qpe_precision_guarantee

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

defaults.assumptions = qpe_precision_guarantee.all_conditions()

defaults.assumptions:

_precision_guarantee

 ⊢  

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

(_precision_guarantee.generalize(
            qpe_precision_guarantee.instance_param_lists(),
            conditions=qpe_precision_guarantee.all_conditions())
       .inner_expr().instance_expr.instance_expr.instance_expr.with_wrapping()
       .inner_expr().instance_expr.instance_expr.with_wrapping())

 ⊢  

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

%qed

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

	step type	requirements	statement
0	literal generalization	1	⊢
1	conjecture		⊢
	proveit.physics.quantum.QPE._precision_guarantee