Executing the unconditional-estimator reduction in polynomial time

This module proves that encoded polynomial-time implementations of the two ordinary queries, validity check, numerical rulers, and ordinary estimator induce a polynomial-time threshold language for the adjusted conditional estimator.

@[simp]

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.lengthLeFlag_eq_true_iff (first second : List Bool) : lengthLeFlag first second = [true] ↔ first.length ≤ second.length

Length comparison produces true exactly for the intended inequality.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.lengthLeFlag_mem_FP {first second : List Bool → List Bool} (hfirst : first ∈ FP) (hsecond : second ∈ FP) : (fun (bits : List Bool) => lengthLeFlag (first bits) (second bits)) ∈ FP

Comparing the lengths of two polynomial-time string functions is itself polynomial-time.

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.encodedEstimatorOfGapSolver (decide : List Bool → Bool) (hdecide : (fun (bits : List Bool) => [decide bits]) ∈ FP) : EncodedEstimator (GapMINKT.Logarithmic.Efficient.executableEstimator decide)

Package the explicit Fact 3.4 threshold sweep as the encoded ordinary estimator consumed by the unconditional two-query reduction.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.EncodedPlan.decisionString_mem_FP {plan : Plan} (encodedPlan : EncodedPlan plan) {estimate : GapMINKT.Logarithmic.Estimator} (encodedEstimator : EncodedEstimator estimate) : encodedPlan.decisionString encodedEstimator ∈ FP

The complete encoded two-query threshold test is polynomial-time.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.EncodedPlan.decisionString_mem_firstBitOne_iff {plan : Plan} (encodedPlan : EncodedPlan plan) {estimate : GapMINKT.Logarithmic.Estimator} (encodedEstimator : EncodedEstimator estimate) (bits : List Bool) : encodedPlan.decisionString encodedEstimator bits ∈ Language.firstBitOne ↔ bits ∈ estimatorLanguage (plan.components estimate).estimate

The encoded test accepts exactly the induced conditional estimator language, including rejection of malformed source codes.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.EncodedPlan.estimatorLanguage_mem_P {plan : Plan} (encodedPlan : EncodedPlan plan) {estimate : GapMINKT.Logarithmic.Estimator} (encodedEstimator : EncodedEstimator estimate) : estimatorLanguage (plan.components estimate).estimate ∈ P

Encoded implementations discharge the algorithmic P obligation in the unconditional-estimator reduction.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Compatible.mem_PromiseP_of_implementations {ordinaryTapes conditionalTapes : ℕ} {plan : Plan} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {ordinaryParameters : GapMINKT.Logarithmic.Parameters} {conditionalParameters : Parameters} {soiClock soiLoss : ℕ → ℕ} (hcompatible : Compatible plan ordinaryMachine conditionalMachine ordinaryParameters conditionalParameters soiClock soiLoss) {ordinaryEstimate : GapMINKT.Logarithmic.Estimator} (hestimate : ordinaryEstimate.SatisfiesBounds ordinaryMachine ordinaryParameters) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine soiClock soiLoss) (hwidening : conditionalParameters.IsWidening) (encodedPlan : EncodedPlan plan) (encodedEstimator : EncodedEstimator ordinaryEstimate) : GapMINCKT ordinaryMachine conditionalMachine conditionalParameters hwidening ∈ PromiseP

A compatible SoI reduction with encoded implementations places the exact conditional gap promise in PromiseP; no separate language-membership premise is needed.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Compatible.mem_PromiseP_of_implementationsOnQueries {ordinaryTapes conditionalTapes : ℕ} {plan : Plan} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {ordinaryParameters : GapMINKT.Logarithmic.Parameters} {conditionalParameters : Parameters} {soiClock soiLoss : ℕ → ℕ} (hcompatible : Compatible plan ordinaryMachine conditionalMachine ordinaryParameters conditionalParameters soiClock soiLoss) {ordinaryEstimate : GapMINKT.Logarithmic.Estimator} (hestimate : ordinaryEstimate.SatisfiesBoundsOn ordinaryMachine ordinaryParameters plan.IsEstimatorQuery) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine soiClock soiLoss) (hwidening : conditionalParameters.IsWidening) (encodedPlan : EncodedPlan plan) (encodedEstimator : EncodedEstimator ordinaryEstimate) : GapMINCKT ordinaryMachine conditionalMachine conditionalParameters hwidening ∈ PromiseP

The implementation theorem also needs estimator correctness only on the plan's two ordinary-query families.