Auxiliary-unary MINKT instances -- proof internals

Proofs that auxiliary-unary samples are exact canonical MINKT codes, together with their machine-relative membership and point-mass characterizations.

theorem Complexity.AuxiliaryUnarySeed.minktInstance_output_internal {m : ℕ} (seed : AuxiliaryUnarySeed m) : seed.minktInstance.output = seed.binary

theorem Complexity.AuxiliaryUnarySeed.minktInstance_time_internal {m : ℕ} (seed : AuxiliaryUnarySeed m) : seed.minktInstance.time = m - seed.split

theorem Complexity.AuxiliaryUnarySeed.minktInstance_output_length_internal {m : ℕ} (seed : AuxiliaryUnarySeed m) : seed.minktInstance.output.length = seed.split

theorem Complexity.AuxiliaryUnarySeed.minktInstance_time_pos_internal {m : ℕ} (hm : 0 < m) (seed : AuxiliaryUnarySeed m) : 0 < seed.minktInstance.time

theorem Complexity.AuxiliaryUnarySeed.encode_minktInstance_internal {m : ℕ} (seed : AuxiliaryUnarySeed m) : seed.minktInstance.encode = seed.sample

theorem Complexity.AuxiliaryUnarySeed.decode?_sample_internal {m : ℕ} (seed : AuxiliaryUnarySeed m) : MINKT.Instance.decode? seed.sample = some seed.minktInstance

theorem Complexity.AuxiliaryUnarySeed.sample_mem_minkt_iff_internal {tapes m : ℕ} (seed : AuxiliaryUnarySeed m) (machine : TM tapes) (threshold : ℕ → ℕ) : seed.sample ∈ MINKT machine threshold ↔ seed.minktInstance.IsBelow machine threshold

theorem Complexity.AuxiliaryUnarySeed.sample_mem_minkt_iff_complexity_internal {tapes m : ℕ} (seed : AuxiliaryUnarySeed m) (machine : TM tapes) (threshold : ℕ → ℕ) : seed.sample ∈ MINKT machine threshold ↔ machine.timeBoundedKolmogorovComplexity seed.binary (m - seed.split) < ↑(threshold seed.split)

theorem Complexity.AuxiliaryUnarySeed.sample_mem_minkt_iff_mem_strictlyCompressible_internal {tapes m : ℕ} (seed : AuxiliaryUnarySeed m) (machine : TM tapes) (threshold : ℕ → ℕ) : seed.sample ∈ MINKT machine threshold ↔ seed.binaryBits ∈ machine.timeBoundedStrictlyCompressibleStrings seed.split (m - seed.split) (threshold seed.split)

theorem Complexity.FiniteEnsemble.languageProbability_auxiliaryUnary_minkt_internal {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (m : ℕ) : auxiliaryUnary.languageProbability (MINKT machine threshold) m = auxiliaryUnaryMINKTProbability machine threshold m

theorem Complexity.FiniteEnsemble.probability_auxiliaryUnary_minkt_eq_average_internal {tapes m : ℕ} (hm : 0 < m) (machine : TM tapes) (threshold : ℕ → ℕ) : auxiliaryUnaryMINKTProbability machine threshold m = 1 / ↑m * ∑ n : Fin m, eventProb (machine.timeBoundedStrictlyCompressibleStrings (↑n) (m - ↑n) (threshold ↑n))

theorem Complexity.FiniteEnsemble.probability_auxiliaryUnary_minkt_le_average_incompressibility_internal {tapes m : ℕ} (hm : 0 < m) (machine : TM tapes) (threshold : ℕ → ℕ) : auxiliaryUnaryMINKTProbability machine threshold m ≤ 1 / ↑m * ∑ n : Fin m, ↑(2 ^ threshold ↑n - 1) / 2 ^ ↑n

theorem Complexity.FiniteEnsemble.probability_auxiliaryUnary_minkt_le_of_pointwise_internal {tapes m : ℕ} (hm : 0 < m) (machine : TM tapes) (threshold : ℕ → ℕ) (bound : ℚ) (hbound : ∀ (n : Fin m), ↑(2 ^ threshold ↑n - 1) / 2 ^ ↑n ≤ bound) : auxiliaryUnaryMINKTProbability machine threshold m ≤ bound

theorem Complexity.FiniteEnsemble.mass_auxiliaryUnary_minktInstance_internal {m n : ℕ} (hn : n < m) (output : Fin n → Bool) : auxiliaryUnary.mass m { output := List.ofFn output, time := m - n }.encode = 1 / (↑m * 2 ^ n)

theorem Complexity.MINKT.one_sub_auxiliaryUnaryProbability_sub_failure_le_reject_internal {tapes m : ℕ} {machine : TM tapes} {threshold : ℕ → ℕ} {A : HeuristicAlgorithm} (herrorless : A.IsErrorlessFor (MINKT machine threshold)) : 1 - FiniteEnsemble.auxiliaryUnaryMINKTProbability machine threshold m - HeuristicAlgorithm.failureProbability FiniteEnsemble.auxiliaryUnary A m ≤ HeuristicAlgorithm.answerProbability FiniteEnsemble.auxiliaryUnary A HeuristicAnswer.reject m

theorem Complexity.MINKT.auxiliaryUnary_rejectProbability_ge_average_internal {tapes m : ℕ} (hm : 0 < m) {machine : TM tapes} {threshold : ℕ → ℕ} {A : HeuristicAlgorithm} (herrorless : A.IsErrorlessFor (MINKT machine threshold)) : 1 - 1 / ↑m * ∑ n : Fin m, ↑(2 ^ threshold ↑n - 1) / 2 ^ ↑n - HeuristicAlgorithm.failureProbability FiniteEnsemble.auxiliaryUnary A m ≤ HeuristicAlgorithm.answerProbability FiniteEnsemble.auxiliaryUnary A HeuristicAnswer.reject m

theorem Complexity.MINKT.auxiliaryUnary_rejectProbability_ge_of_pointwise_internal {tapes m : ℕ} (hm : 0 < m) {machine : TM tapes} {threshold : ℕ → ℕ} {A : HeuristicAlgorithm} (low failure : ℚ) (herrorless : A.IsErrorlessFor (MINKT machine threshold)) (hlow : ∀ (n : Fin m), ↑(2 ^ threshold ↑n - 1) / 2 ^ ↑n ≤ low) (hfailure : HeuristicAlgorithm.failureProbability FiniteEnsemble.auxiliaryUnary A m ≤ failure) : 1 - low - failure ≤ HeuristicAlgorithm.answerProbability FiniteEnsemble.auxiliaryUnary A HeuristicAnswer.reject m