Gap MINKT -- proof internals

Proofs of codec exactness, direct program characterizations, widening-based disjointness, and totality of the finite-complexity search relation.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Complexity.GapMINKT.exists_searchRelation_iff_internal {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 ≠ ⊤

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

theorem Complexity.GapMINKT.exists_encodedSearchRelation_encode_iff_internal {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 ≠ ⊤

theorem Complexity.GapMINKT.encodedSearchRelation_length_le_polynomial_internal {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))

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

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

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

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

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

theorem Complexity.GapMINKT.decisionOfSearch_eq_true_of_mem_yesLanguage_internal {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

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