Logarithmic-gap MINKT -- proof internals

theorem Complexity.GapMINKT.Logarithmic.Parameters.identity_isAdmissible_internal : identity.IsAdmissible

theorem Complexity.GapMINKT.Logarithmic.transformedTime_ge_internal (parameters : Parameters) (hwidening : parameters.IsWidening) (inst : MINKT.Instance) : inst.time ≤ parameters.transformedTime inst

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

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

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

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

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

theorem Complexity.GapMINKT.Logarithmic.estimator_le_threshold_of_isYes_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds machine parameters) (inst : Instance) (hyes : inst.IsYes machine) : estimate inst.base ≤ inst.threshold

theorem Complexity.GapMINKT.Logarithmic.threshold_lt_estimator_of_isNo_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds machine parameters) (inst : Instance) (hno : IsNo inst machine parameters) : inst.threshold < estimate inst.base

theorem Complexity.GapMINKT.Logarithmic.estimatorLanguage_mem_encode_iff_internal (estimate : Estimator) (inst : Instance) : inst.encode ∈ estimatorLanguage estimate ↔ estimate inst.base ≤ inst.threshold

theorem Complexity.GapMINKT.Logarithmic.decisionOfEstimator_eq_true_iff_internal (estimate : Estimator) (bits : List Bool) : decisionOfEstimator estimate bits = true ↔ bits ∈ estimatorLanguage estimate

theorem Complexity.GapMINKT.Logarithmic.yesLanguage_subset_estimatorLanguage_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds machine parameters) : yesLanguage machine ⊆ estimatorLanguage estimate

theorem Complexity.GapMINKT.Logarithmic.disjoint_estimatorLanguage_noLanguage_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds machine parameters) : Disjoint (estimatorLanguage estimate) (noLanguage machine parameters)

theorem Complexity.GapMINKT.Logarithmic.decisionOfEstimator_eq_true_of_mem_yesLanguage_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds machine parameters) {bits : List Bool} (hyes : bits ∈ yesLanguage machine) : decisionOfEstimator estimate bits = true

theorem Complexity.GapMINKT.Logarithmic.decisionOfEstimator_eq_false_of_mem_noLanguage_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds machine parameters) {bits : List Bool} (hno : bits ∈ noLanguage machine parameters) : decisionOfEstimator estimate bits = false

theorem Complexity.GapMINKT.Logarithmic.thresholdInstance_base_internal (inst : MINKT.Instance) (threshold : ℕ) : (thresholdInstance inst threshold).base = inst

theorem Complexity.GapMINKT.Logarithmic.firstAcceptedThreshold_spec_of_accepted_internal (decide : List Bool → Bool) (inst : MINKT.Instance) {cap threshold : ℕ} (hthreshold : threshold ≤ cap) (haccept : decide (thresholdInstance inst threshold).encode = true) : decide (thresholdInstance inst (firstAcceptedThreshold decide inst cap)).encode = true ∧ firstAcceptedThreshold decide inst cap ≤ threshold

theorem Complexity.GapMINKT.Logarithmic.timeSearchEstimator_satisfiesBoundsAt_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {decide : List Bool → Bool} (haccept : ∀ bits ∈ yesLanguage machine, decide bits = true) (hreject : ∀ bits ∈ noLanguage machine parameters, decide bits = false) (inst : MINKT.Instance) (hfinite : machine.timeBoundedKolmogorovComplexity inst.output inst.time ≠ ⊤) : ↑(timeSearchEstimator decide inst) ≤ machine.timeBoundedKolmogorovComplexity inst.output inst.time ∧ machine.timeBoundedKolmogorovComplexity inst.output (parameters.transformedTime inst) ≤ ↑(timeSearchEstimator decide inst + parameters.logarithmicSlack inst)

theorem Complexity.GapMINKT.Logarithmic.timeSearchEstimator_satisfiesBoundsOn_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {decide : List Bool → Bool} {eligible : MINKT.Instance → Prop} (haccept : ∀ bits ∈ yesLanguage machine, decide bits = true) (hreject : ∀ bits ∈ noLanguage machine parameters, decide bits = false) (hfinite : ∀ (inst : MINKT.Instance), eligible inst → machine.timeBoundedKolmogorovComplexity inst.output inst.time ≠ ⊤) : (timeSearchEstimator decide).SatisfiesBoundsOn machine parameters eligible

theorem Complexity.GapMINKT.Logarithmic.timeSearchEstimator_satisfiesBounds_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} {decide : List Bool → Bool} (haccept : ∀ bits ∈ yesLanguage machine, decide bits = true) (hreject : ∀ bits ∈ noLanguage machine parameters, decide bits = false) (hfinite : ∀ (inst : MINKT.Instance), machine.timeBoundedKolmogorovComplexity inst.output inst.time ≠ ⊤) : (timeSearchEstimator decide).SatisfiesBounds machine parameters