Gap MINKT -- definitions

The decision instance (x, 1^t, 1^s) has the following promised sides:

• yes: C_U^t(x) <= s;
• no: C_U^(tau(|x|,t))(x) > sigma(|x|,s).

The description transformation sigma and clock transformation tau are independent parameters. Parameters.IsWidening is kept as a separate property: it is required to prove the two sides disjoint, but not to state either side or the associated search relation.

The search relation follows the optimization form: relative to the exact finite value C_U^t(x) = s, output a program of length at most sigma(|x|,s) that produces x within tau(|x|,t) steps.

structure Complexity.GapMINKT.Parameters : Type

Independent quantitative transformations for description loss and clock blow-up.

• description : ℕ → ℕ → ℕ

  Allowed output-program length from input length and source complexity.

• clock : ℕ → ℕ → ℕ

  Allowed target clock from input length and source clock.

def Complexity.GapMINKT.Parameters.IsWidening (parameters : Parameters) : Prop

Both resources weakly increase. This suffices to make the gap sides disjoint and to reuse an exact source description as a search witness.

Equations

• parameters.IsWidening = ((∀ (length threshold : ℕ), threshold ≤ parameters.description length threshold) ∧ ∀ (length time : ℕ), time ≤ parameters.clock length time)

def Complexity.GapMINKT.Parameters.DescriptionMonotone (parameters : Parameters) : Prop

For each output length, increasing the source threshold cannot decrease the allowed target description length.

Equations

• parameters.DescriptionMonotone = ∀ (length : ℕ), Monotone (parameters.description length)

def Complexity.GapMINKT.Parameters.DescriptionPolyBound (parameters : Parameters) : Prop

The description-loss map is bounded by one polynomial in the sum of the output length and source optimum.

Equations

• parameters.DescriptionPolyBound = ∃ (polynomial : Polynomial ℕ), ∀ (length optimum : ℕ), parameters.description length optimum ≤ Polynomial.eval (length + optimum) polynomial

def Complexity.GapMINKT.SourceComplexityPolyBound {tapes : ℕ} (machine : TM tapes) : Prop

Finite source complexity values are polynomially bounded by the canonical (x,1^t) input length. This names the precise input-size bridge needed for optimization-search balance; input locality proves it for every current sequential-input TM, with the identity polynomial.

Equations

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

structure Complexity.GapMINKT.Instance : Type

A decoded gap-decision instance (x, 1^t, 1^s).

• output : List Bool

  String whose bounded description complexity is measured.

• time : ℕ

  Source primitive machine-step budget.

• threshold : ℕ

  Source description-length threshold.

def Complexity.GapMINKT.Instance.base (inst : Instance) : MINKT.Instance

Forget the decision threshold, retaining the underlying MINKT instance.

Equations

• inst.base = { output := inst.output, time := inst.time }

def Complexity.GapMINKT.Instance.unaryThreshold (inst : Instance) : List Bool

Unary encoding of the decision threshold.

Equations

• inst.unaryThreshold = List.replicate inst.threshold true

def Complexity.GapMINKT.Instance.encode (inst : Instance) : List Bool

Canonical nested-pair encoding of (x, 1^t, 1^s).

Equations

• inst.encode = Complexity.pair inst.base.encode inst.unaryThreshold

def Complexity.GapMINKT.Instance.decode? (bits : List Bool) : Option Instance

Decode one canonical gap instance, rejecting malformed pairing and every non-unary threshold field.

Equations

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

def Complexity.GapMINKT.Instance.withThreshold (inst : Instance) (threshold : ℕ) : Instance

Replace only the source description threshold.

Equations

• inst.withThreshold threshold = { output := inst.output, time := inst.time, threshold := threshold }

def Complexity.GapMINKT.Instance.IsYes {tapes : ℕ} (inst : Instance) (machine : TM tapes) : Prop

Promised yes condition C_U^t(x) <= s.

Equations

• inst.IsYes machine = (machine.timeBoundedKolmogorovComplexity inst.output inst.time ≤ ↑inst.threshold)

def Complexity.GapMINKT.Instance.IsNo {tapes : ℕ} (inst : Instance) (machine : TM tapes) (parameters : Parameters) : Prop

Promised no condition C_U^(tau(|x|,t))(x) > sigma(|x|,s).

Equations

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

def Complexity.GapMINKT.Instance.IsRelaxedWitness {tapes : ℕ} (inst : Instance) (machine : TM tapes) (parameters : Parameters) (program : List Bool) : Prop

A program witnessing the relaxed target resources of a gap instance.

Equations

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

def Complexity.GapMINKT.yesLanguage {tapes : ℕ} (machine : TM tapes) : Language

Canonically encoded promised yes language. Malformed codes are outside the promise rather than being assigned to the no side.

Equations

• Complexity.GapMINKT.yesLanguage machine = {bits : List Bool | match Complexity.GapMINKT.Instance.decode? bits with | some inst => inst.IsYes machine | none => False}

def Complexity.GapMINKT.noLanguage {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) : Language

Canonically encoded promised no language for the quantitative gap.

Equations

• Complexity.GapMINKT.noLanguage machine parameters = {bits : List Bool | match Complexity.GapMINKT.Instance.decode? bits with | some inst => inst.IsNo machine parameters | none => False}

def Complexity.GapMINKT.YesWitnessRelation {tapes : ℕ} (machine : TM tapes) (bits program : List Bool) : Prop

Direct source-threshold witness relation for the promised yes language.

Equations

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

def Complexity.GapMINKT.SearchRelation {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (inst : MINKT.Instance) (program : List Bool) : Prop

Search approximation relative to the exact finite source complexity.

On input (x, 1^t), a related program has length at most sigma(|x|, C_U^t(x)) and produces x within tau(|x|,t).

Equations

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

def Complexity.GapMINKT.EncodedSearchRelation {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (bits program : List Bool) : Prop

Canonical binary-input form of the optimization search relation. Malformed (x,1^t) codes have no related output.

Equations

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

@[reducible, inline]

abbrev Complexity.GapMINKT.SearchAlgorithm : Type

Semantic search algorithm returning a candidate program from (x,1^t).

Equations

• Complexity.GapMINKT.SearchAlgorithm = (Complexity.MINKT.Instance → List Bool)

def Complexity.GapMINKT.SolvesSearchOnFinite {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (search : SearchAlgorithm) : Prop

A search algorithm satisfies the approximation relation on every input whose source time-bounded complexity is finite.

Equations

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

def Complexity.GapMINKT.verifyRelaxedWitness {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (inst : Instance) (program : List Bool) : Bool

Executably check whether a candidate meets a gap instance's relaxed target resources.

Equations

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

def Complexity.GapMINKT.decisionOfSearch {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (search : SearchAlgorithm) : List Bool → Bool

Convert a search algorithm into a total Boolean decision function by decoding a gap instance and checking the returned candidate program.

Equations

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