Gap conditional MinKT -- proof internals

theorem Complexity.GapMINCKT.Parameters.identity_isAdmissible_internal : identity.IsAdmissible

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

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

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

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

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

theorem Complexity.GapMINCKT.Instance.length_encode_internal (inst : Instance) : inst.encode.length = 4 * inst.output.length + 4 * inst.condition.length + 2 * inst.time + inst.threshold + 10

theorem Complexity.GapMINCKT.Instance.laterTime_ge_internal (parameters : Parameters) (hwidening : parameters.IsWidening) (inst : Instance) : inst.time ≤ inst.laterTime parameters

theorem Complexity.GapMINCKT.Instance.conditionDepth_add_later_internal {ordinaryTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (parameters : Parameters) (hwidening : parameters.IsWidening) (inst : Instance) : inst.conditionDepth ordinaryMachine parameters + ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition (inst.laterTime parameters) = ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition inst.time

theorem Complexity.GapMINCKT.Instance.isYes_iff_exists_adjustedWitness_internal {ordinaryTapes conditionalTapes : ℕ} (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) : inst.IsYes ordinaryMachine conditionalMachine parameters ↔ ∃ (program : List Bool), inst.IsAdjustedWitness ordinaryMachine conditionalMachine parameters program

theorem Complexity.GapMINCKT.Instance.isYes_implies_base_isAtMost_internal {ordinaryTapes conditionalTapes : ℕ} (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (hyes : inst.IsYes ordinaryMachine conditionalMachine parameters) : inst.base.IsAtMost conditionalMachine inst.threshold

theorem Complexity.GapMINCKT.Instance.isNo_iff_no_relaxedWitness_internal {conditionalTapes : ℕ} (inst : Instance) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) : inst.IsNo conditionalMachine parameters ↔ ¬∃ (program : List Bool), inst.IsRelaxedWitness conditionalMachine parameters program

theorem Complexity.GapMINCKT.Instance.IsYes.withThreshold_mono_internal {ordinaryTapes conditionalTapes : ℕ} (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) {first second : ℕ} (hthreshold : first ≤ second) (hyes : (inst.withThreshold first).IsYes ordinaryMachine conditionalMachine parameters) : (inst.withThreshold second).IsYes ordinaryMachine conditionalMachine parameters

theorem Complexity.GapMINCKT.Instance.IsNo.withThreshold_anti_internal {conditionalTapes : ℕ} (inst : Instance) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) {first second : ℕ} (hthreshold : first ≤ second) (hno : (inst.withThreshold second).IsNo conditionalMachine parameters) : (inst.withThreshold first).IsNo conditionalMachine parameters

theorem Complexity.GapMINCKT.Instance.not_isNo_of_isYes_internal {ordinaryTapes conditionalTapes : ℕ} (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (hwidening : parameters.IsWidening) (hyes : inst.IsYes ordinaryMachine conditionalMachine parameters) : ¬inst.IsNo conditionalMachine parameters

theorem Complexity.GapMINCKT.estimator_le_threshold_of_isYes_internal {ordinaryTapes conditionalTapes : ℕ} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) (inst : Instance) (hyes : inst.IsYes ordinaryMachine conditionalMachine parameters) : estimate inst.base ≤ inst.threshold

theorem Complexity.GapMINCKT.threshold_lt_estimator_of_isNo_internal {ordinaryTapes conditionalTapes : ℕ} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) (inst : Instance) (hno : inst.IsNo conditionalMachine parameters) : inst.threshold < estimate inst.base

theorem Complexity.GapMINCKT.yesLanguage_mem_encode_iff_internal {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (inst : Instance) : inst.encode ∈ yesLanguage ordinaryMachine conditionalMachine parameters ↔ inst.IsYes ordinaryMachine conditionalMachine parameters

theorem Complexity.GapMINCKT.noLanguage_mem_encode_iff_internal {conditionalTapes : ℕ} (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (inst : Instance) : inst.encode ∈ noLanguage conditionalMachine parameters ↔ inst.IsNo conditionalMachine parameters

theorem Complexity.GapMINCKT.disjoint_yesLanguage_noLanguage_internal {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (hwidening : parameters.IsWidening) : Disjoint (yesLanguage ordinaryMachine conditionalMachine parameters) (noLanguage conditionalMachine parameters)

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

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

theorem Complexity.GapMINCKT.yesLanguage_subset_estimatorLanguage_internal {ordinaryTapes conditionalTapes : ℕ} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) : yesLanguage ordinaryMachine conditionalMachine parameters ⊆ estimatorLanguage estimate

theorem Complexity.GapMINCKT.disjoint_estimatorLanguage_noLanguage_internal {ordinaryTapes conditionalTapes : ℕ} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) : Disjoint (estimatorLanguage estimate) (noLanguage conditionalMachine parameters)

theorem Complexity.GapMINCKT.decisionOfEstimator_eq_true_of_mem_yesLanguage_internal {ordinaryTapes conditionalTapes : ℕ} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) {bits : List Bool} (hyes : bits ∈ yesLanguage ordinaryMachine conditionalMachine parameters) : decisionOfEstimator estimate bits = true

theorem Complexity.GapMINCKT.decisionOfEstimator_eq_false_of_mem_noLanguage_internal {ordinaryTapes conditionalTapes : ℕ} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) {bits : List Bool} (hno : bits ∈ noLanguage conditionalMachine parameters) : decisionOfEstimator estimate bits = false