Encoded implementations of the unconditional-estimator reduction

These contracts expose the algorithmic content hidden by the semantic assumption that an induced estimator language belongs to P. Natural-valued estimates and corrections are represented extensionally by output length. The plan implementation builds the two canonical ordinary MINKT queries, recognizes valid conditional-gap codes, and materializes the correction and threshold as length rulers.

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.lengthLeFlag (first second : List Bool) : List Bool

A one-bit flag recording whether the first string is no longer than the second.

Equations

• Complexity.GapMINCKT.DifferenceEstimator.Unconditional.lengthLeFlag first second = [decide (first.length ≤ second.length)]

structure Complexity.GapMINCKT.DifferenceEstimator.Unconditional.EncodedEstimator (estimate : GapMINKT.Logarithmic.Estimator) : Type

A polynomial-time implementation of an ordinary numerical estimator. Only the output length is semantically relevant, so the implementation may use any bit contents.

• run : List Bool → List Bool

  Run the estimator on a canonical ordinary MINKT code.

• run_mem_FP : self.run ∈ FP

  The estimator implementation is polynomial-time computable.

• length_run_encode (inst : MINKT.Instance) : (self.run inst.encode).length = estimate inst

  On a canonical input, output length is exactly the numerical estimate.

structure Complexity.GapMINCKT.DifferenceEstimator.Unconditional.EncodedPlan (plan : Plan) : Type

Polynomial-time encoded data needed to execute an unconditional two-query plan. Correctness is required only after the source conditional-gap code successfully decodes; validRuler separately recognizes that domain.

• pairQuery : List Bool → List Bool

  Build the paired ordinary MINKT query.

• conditionQuery : List Bool → List Bool

  Build the condition-only ordinary MINKT query.

• validRuler : List Bool → List Bool

  One-cell ruler on valid source codes and the empty ruler otherwise.

• correctionRuler : List Bool → List Bool

  Materialize the plan's correction as a unary-length ruler.

• thresholdRuler : List Bool → List Bool

  Materialize the source threshold as a unary-length ruler.

• pairQuery_mem_FP : self.pairQuery ∈ FP

  The paired-query builder is polynomial-time computable.

• conditionQuery_mem_FP : self.conditionQuery ∈ FP

  The condition-query builder is polynomial-time computable.

• validRuler_mem_FP : self.validRuler ∈ FP

  The validity ruler is polynomial-time computable.

• correctionRuler_mem_FP : self.correctionRuler ∈ FP

  The correction ruler is polynomial-time computable.

• thresholdRuler_mem_FP : self.thresholdRuler ∈ FP

  The threshold ruler is polynomial-time computable.

• length_validRuler (bits : List Bool) : (self.validRuler bits).length = match Instance.decode? bits with | some _inst => 1 | none => 0

  The validity ruler has length one exactly on successfully decoded codes.

• pairQuery_eq (bits : List Bool) (inst : Instance) : Instance.decode? bits = some inst → self.pairQuery bits = (plan.pairInput inst.base).encode

  A valid source code is mapped to its exact paired query.

• conditionQuery_eq (bits : List Bool) (inst : Instance) : Instance.decode? bits = some inst → self.conditionQuery bits = (plan.conditionInput inst.base).encode

  A valid source code is mapped to its exact condition query.

• length_correctionRuler (bits : List Bool) (inst : Instance) : Instance.decode? bits = some inst → (self.correctionRuler bits).length = plan.correction inst.base

  The correction ruler has the planned length on valid inputs.

• length_thresholdRuler (bits : List Bool) (inst : Instance) : Instance.decode? bits = some inst → (self.thresholdRuler bits).length = inst.threshold

  The threshold ruler recovers the source threshold length.

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.EncodedPlan.decisionString {plan : Plan} (encodedPlan : EncodedPlan plan) {estimate : GapMINKT.Logarithmic.Estimator} (encodedEstimator : EncodedEstimator estimate) : List Bool → List Bool

Execute the adjusted-difference threshold test entirely through string functions. The right ruler has length D + correction + threshold; comparison with the joint-estimate ruler is equivalent to J - D - correction ≤ threshold. Truncation by validRuler rejects malformed source codes.

Equations

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