Difference estimators for conditional gap MinKT #
This module packages the cancellation step in the estimator construction of
Hirahara's Proposition 6.2. A joint estimate, condition estimate, and explicit
correction produce a conditional estimator by natural subtraction. The two
pre-cancellation accounting inequalities are sufficient to prove the exact
GapMINCKT estimator sandwich and hence solve the promise.
@[simp]
theorem
Complexity.GapMINCKT.DifferenceEstimator.estimate_apply
(components : DifferenceEstimator)
(inst : MINCKT.Instance)
:
components.estimate inst = components.minuend inst - components.subtrahend inst - components.correction inst
The adjusted difference expands to its three numerical components.
theorem
Complexity.GapMINCKT.DifferenceEstimator.SatisfiesAccounting.satisfiesBounds
{ordinaryTapes conditionalTapes : ℕ}
{components : DifferenceEstimator}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{parameters : Parameters}
(haccounting : components.SatisfiesAccounting ordinaryMachine conditionalMachine parameters)
:
components.estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters
The two pre-cancellation accounting inequalities imply the exact conditional-complexity estimator sandwich.
theorem
Complexity.GapMINCKT.DifferenceEstimator.SatisfiesAccounting.solvedBy
{ordinaryTapes conditionalTapes : ℕ}
{components : DifferenceEstimator}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{parameters : Parameters}
(haccounting : components.SatisfiesAccounting ordinaryMachine conditionalMachine parameters)
(hwidening : parameters.IsWidening)
:
(GapMINCKT ordinaryMachine conditionalMachine parameters hwidening).SolvedBy (decisionOfEstimator components.estimate)
Thresholding an accounting-certified adjusted difference solves the exact conditional gap promise.
theorem
Complexity.GapMINCKT.DifferenceEstimator.SatisfiesAccounting.mem_PromiseP
{ordinaryTapes conditionalTapes : ℕ}
{components : DifferenceEstimator}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{parameters : Parameters}
(haccounting : components.SatisfiesAccounting ordinaryMachine conditionalMachine parameters)
(hwidening : parameters.IsWidening)
(hpolynomial : estimatorLanguage components.estimate ∈ P)
:
Polynomial-time thresholding of an accounting-certified adjusted
difference supplies a PromiseP completion.