Gap MINKT

This module exposes Hirahara's quantitative decision promise and associated search relation with separate description-loss and clock-blow-up maps.

For a canonical input (x, 1^t, 1^s), the promise distinguishes C_U^t(x) <= s from C_U^(tau(|x|,t))(x) > sigma(|x|,s). Malformed encodings and intermediate-gap instances lie outside the promise.

@[simp]

theorem Complexity.GapMINKT.Instance.length_unaryThreshold (inst : Instance) : inst.unaryThreshold.length = inst.threshold

The unary threshold has exactly the represented length.

@[simp]

theorem Complexity.GapMINKT.Instance.decode?_encode (inst : Instance) : decode? inst.encode = some inst

Every canonical gap instance decodes exactly.

theorem Complexity.GapMINKT.Instance.decode?_eq_some_iff (bits : List Bool) (inst : Instance) : decode? bits = some inst ↔ bits = inst.encode

Exact decoding accepts precisely canonical gap encodings.

theorem Complexity.GapMINKT.Instance.decode?_eq_none_iff (bits : List Bool) : decode? bits = none ↔ ¬∃ (inst : Instance), bits = inst.encode

Decoding rejects exactly the noncanonical strings.

theorem Complexity.GapMINKT.Instance.encode_injective : Function.Injective encode

Canonical gap-instance encoding is injective.

@[simp]

theorem Complexity.GapMINKT.Instance.length_encode (inst : Instance) : inst.encode.length = 4 * inst.output.length + 2 * inst.time + inst.threshold + 6

Exact nested-pair code length for (x, 1^t, 1^s).

theorem Complexity.GapMINKT.Instance.isYes_iff_exists_program {tapes : ℕ} (inst : Instance) (machine : TM tapes) : inst.IsYes machine ↔ ∃ (program : List Bool), program.length ≤ inst.threshold ∧ machine.ProducesInTime program inst.output inst.time

The yes condition is equivalent to a source-short program within the source clock.

theorem Complexity.GapMINKT.Instance.isNo_iff_no_relaxedWitness {tapes : ℕ} (inst : Instance) (machine : TM tapes) (parameters : Parameters) : inst.IsNo machine parameters ↔ ¬∃ (program : List Bool), inst.IsRelaxedWitness machine parameters program

The no condition says exactly that no program meets both relaxed target resources.

theorem Complexity.GapMINKT.Instance.not_isNo_of_isYes {tapes : ℕ} (inst : Instance) (machine : TM tapes) (parameters : Parameters) (hwidening : parameters.IsWidening) (hyes : inst.IsYes machine) : ¬inst.IsNo machine parameters

Widening both resources prevents any yes-instance from also satisfying the no condition.

@[simp]

theorem Complexity.GapMINKT.mem_yesLanguage_encode_iff {tapes : ℕ} (machine : TM tapes) (inst : Instance) : inst.encode ∈ yesLanguage machine ↔ inst.IsYes machine

Canonical yes-language membership is the source bounded-complexity inequality.

@[simp]

theorem Complexity.GapMINKT.mem_noLanguage_encode_iff {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (inst : Instance) : inst.encode ∈ noLanguage machine parameters ↔ inst.IsNo machine parameters

Canonical no-language membership is the relaxed lower-bound inequality.

theorem Complexity.GapMINKT.disjoint_yesLanguage_noLanguage {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (hwidening : parameters.IsWidening) : Disjoint (yesLanguage machine) (noLanguage machine parameters)

Under widening, the two encoded gap languages are disjoint.

theorem Complexity.GapMINKT.mem_yesLanguage_iff_exists_program {tapes : ℕ} (machine : TM tapes) (bits : List Bool) : bits ∈ yesLanguage machine ↔ ∃ (program : List Bool), YesWitnessRelation machine bits program

Encoded yes membership is exactly existence of a raw source program witness.

theorem Complexity.GapMINKT.yesWitnessRelation_length_le_input {tapes : ℕ} (machine : TM tapes) {bits program : List Bool} (hrelation : YesWitnessRelation machine bits program) : program.length ≤ bits.length

Every valid source program is no longer than its canonical unary-threshold instance code.

theorem Complexity.GapMINKT.yesWitnessRelation_polyBalanced {tapes : ℕ} (machine : TM tapes) : PolyBalanced (YesWitnessRelation machine)

The direct source-program witness relation for GapMINKT yes-instances is linearly balanced, with the identity polynomial as its bound.

theorem Complexity.GapMINKT.yesWitnessRelation_mem_FNP_of_pairLang_mem_P {tapes : ℕ} (machine : TM tapes) (hverifier : pairLang (YesWitnessRelation machine) ∈ P) : YesWitnessRelation machine ∈ FNP

Once its paired verifier language is in P, the direct GapMINKT yes-witness relation belongs to FNP; polynomial balance is unconditional.

theorem Complexity.GapMINKT.exists_searchRelation_iff {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (hwidening : parameters.IsWidening) (inst : MINKT.Instance) : (∃ (program : List Bool), SearchRelation machine parameters inst program) ↔ machine.timeBoundedKolmogorovComplexity inst.output inst.time ≠ ⊤

The optimization search relation has a witness exactly when the source time-bounded complexity is finite.

@[simp]

theorem Complexity.GapMINKT.encodedSearchRelation_encode_iff {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (inst : MINKT.Instance) (program : List Bool) : EncodedSearchRelation machine parameters inst.encode program ↔ SearchRelation machine parameters inst program

On canonical (x,1^t) inputs, the encoded and semantic optimization search relations agree exactly.

theorem Complexity.GapMINKT.exists_encodedSearchRelation_encode_iff {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (hwidening : parameters.IsWidening) (inst : MINKT.Instance) : (∃ (program : List Bool), EncodedSearchRelation machine parameters inst.encode program) ↔ machine.timeBoundedKolmogorovComplexity inst.output inst.time ≠ ⊤

The canonical encoded optimization search problem has a solution exactly when the source time-bounded complexity is finite.

theorem Complexity.GapMINKT.encodedSearchRelation_length_le_polynomial {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (descriptionPolynomial sourcePolynomial : Polynomial ℕ) (hdescription : ∀ (length optimum : ℕ), parameters.description length optimum ≤ Polynomial.eval (length + optimum) descriptionPolynomial) (hsource : ∀ (inst : MINKT.Instance) (optimum : ℕ), machine.timeBoundedKolmogorovComplexity inst.output inst.time = ↑optimum → optimum ≤ Polynomial.eval inst.encode.length sourcePolynomial) {bits program : List Bool} (hrelation : EncodedSearchRelation machine parameters bits program) : program.length ≤ Polynomial.eval bits.length (descriptionPolynomial.comp (Polynomial.X + sourcePolynomial))

Explicit composed polynomial bound for every output of the encoded search relation. The description loss is polynomial in |x|+s, while finite source optima are polynomial in the canonical (x,1^t) input length.

theorem Complexity.GapMINKT.encodedSearchRelation_polyBalanced {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (hdescription : parameters.DescriptionPolyBound) (hsource : SourceComplexityPolyBound machine) : PolyBalanced (EncodedSearchRelation machine parameters)

Polynomial description loss and polynomially bounded finite source optima make the canonical optimization search relation polynomially balanced.

theorem Complexity.GapMINKT.sourceComplexityPolyBound {tapes : ℕ} (machine : TM tapes) : SourceComplexityPolyBound machine

Every deterministic machine satisfies the source-complexity input-size bound, with the identity polynomial: finite C_U^t(x) is at most the unary clock t, which is contained in the canonical input.

theorem Complexity.GapMINKT.encodedSearchRelation_polyBalanced_of_description {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (hdescription : parameters.DescriptionPolyBound) : PolyBalanced (EncodedSearchRelation machine parameters)

Polynomial growth of the description-loss map is the only parameter condition needed for polynomial balance of the encoded optimization search relation.

theorem Complexity.GapMINKT.verifyRelaxedWitness_eq_true_iff {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (inst : Instance) (program : List Bool) : verifyRelaxedWitness machine parameters inst program = true ↔ inst.IsRelaxedWitness machine parameters program

The executable relaxed-resource checker accepts exactly valid candidates.

theorem Complexity.GapMINKT.verifyRelaxedWitness_eq_false_iff {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) (inst : Instance) (program : List Bool) : verifyRelaxedWitness machine parameters inst program = false ↔ ¬inst.IsRelaxedWitness machine parameters program

The executable relaxed-resource checker rejects exactly invalid candidates.

theorem Complexity.GapMINKT.decisionOfSearch_eq_true_of_mem_yesLanguage {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {search : SearchAlgorithm} (hdescription : parameters.DescriptionMonotone) (hsearch : SolvesSearchOnFinite machine parameters search) {bits : List Bool} (hyes : bits ∈ yesLanguage machine) : decisionOfSearch machine parameters search bits = true

A correct finite-input search solver makes the search-derived decision function accept every promised yes-instance when sigma is monotone.

theorem Complexity.GapMINKT.decisionOfSearch_eq_false_of_mem_noLanguage {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} (search : SearchAlgorithm) {bits : List Bool} (hno : bits ∈ noLanguage machine parameters) : decisionOfSearch machine parameters search bits = false

The search-derived decision function rejects every promised no-instance, regardless of the search algorithm's behavior there.

def Complexity.GapMINKT {tapes : ℕ} (machine : TM tapes) (parameters : GapMINKT.Parameters) (hwidening : parameters.IsWidening) : PromiseProblem

The widening-certified GapMINKT decision promise.

Equations

• Complexity.GapMINKT machine parameters hwidening = { yesInstances := Complexity.GapMINKT.yesLanguage machine, noInstances := Complexity.GapMINKT.noLanguage machine parameters, disjoint := ⋯ }

@[simp]

theorem Complexity.GapMINKT_yesInstances {tapes : ℕ} (machine : TM tapes) (parameters : GapMINKT.Parameters) (hwidening : parameters.IsWidening) : (GapMINKT machine parameters hwidening).yesInstances = GapMINKT.yesLanguage machine

The promise problem exposes exactly the canonical yes language.

@[simp]

theorem Complexity.GapMINKT_noInstances {tapes : ℕ} (machine : TM tapes) (parameters : GapMINKT.Parameters) (hwidening : parameters.IsWidening) : (GapMINKT machine parameters hwidening).noInstances = GapMINKT.noLanguage machine parameters

The promise problem exposes exactly the canonical no language.

theorem Complexity.GapMINKT_solvedBy_decisionOfSearch {tapes : ℕ} {machine : TM tapes} {parameters : GapMINKT.Parameters} (hwidening : parameters.IsWidening) (hdescription : parameters.DescriptionMonotone) {search : GapMINKT.SearchAlgorithm} (hsearch : GapMINKT.SolvesSearchOnFinite machine parameters search) : (GapMINKT machine parameters hwidening).SolvedBy (GapMINKT.decisionOfSearch machine parameters search)

A search algorithm correct on every finite source instance induces a semantic solver for the widening-certified GapMINKT promise.

theorem Complexity.GapMINKT_mem_PromiseNP_of_yesWitnessRelation_mem_FNP {tapes : ℕ} {machine : TM tapes} {parameters : GapMINKT.Parameters} (hwidening : parameters.IsWidening) (hwitness : NP.WitnessNTMConstruction) (hrelation : GapMINKT.YesWitnessRelation machine ∈ FNP) : GapMINKT machine parameters hwidening ∈ PromiseNP

An FNP implementation of the direct yes-witness relation places GapMINKT in PromiseNP, conditional on the generic guess-and-verify NTM construction.

theorem Complexity.GapMINKT_mem_PromiseNP_of_pairLang_mem_P {tapes : ℕ} {machine : TM tapes} {parameters : GapMINKT.Parameters} (hwidening : parameters.IsWidening) (hwitness : NP.WitnessNTMConstruction) (hverifier : pairLang (GapMINKT.YesWitnessRelation machine) ∈ P) : GapMINKT machine parameters hwidening ∈ PromiseNP

The remaining GapMINKT-specific PromiseNP obligation is a deterministic polynomial-time verifier for the paired direct-witness language.