The auxiliary-unary distribution as canonical MINKT instances

Every seed in Hirahara's auxiliary-unary ensemble samples the canonical MINKT code of its retained binary prefix and remaining unary clock. This module makes that identity explicit and transfers exact decoding, membership, and point-mass facts to MINKT notation.

@[simp]

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

The sampled MINKT output is exactly the retained binary prefix.

@[simp]

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

The sampled MINKT clock fills the part after the retained prefix.

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

The sampled instance's output length is the selected split.

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

Every positive auxiliary-unary slice gives its MINKT instance a positive clock.

@[simp]

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

The auxiliary-unary sample is definitionally the canonical encoding of its MINKT instance.

@[simp]

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

MINKT decoding of every auxiliary-unary sample succeeds exactly.

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

Auxiliary-unary sample membership is membership of the sampled canonical MINKT instance.

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

Expanded sample membership uses the selected prefix length and remaining primitive clock directly.

theorem Complexity.AuxiliaryUnarySeed.sample_mem_minkt_iff_mem_strictlyCompressible {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)

The MINKT event of a seed is exactly membership of its retained prefix in the corresponding fixed-length strict-compressibility set.

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

The generic language-mass definition agrees exactly with the named MINKT probability under the auxiliary-unary ensemble.

theorem Complexity.FiniteEnsemble.probability_auxiliaryUnary_minkt_eq_average {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))

Exact conditioning identity for strict MINKT under a positive auxiliary-unary slice: its probability is the uniform average of the fixed-length strict-compressibility probabilities over all split lengths.

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

Strict incompressibility bounds the MINKT probability by the average of the sharp per-length ratios (2^r(n) - 1) / 2^n.

theorem Complexity.FiniteEnsemble.probability_auxiliaryUnary_minkt_le_of_pointwise {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

Any common upper bound on the strict incompressibility ratios bounds the entire positive auxiliary-unary slice.

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

Exact point mass of a canonical MINKT instance in the auxiliary-unary ensemble.

theorem Complexity.MINKT.one_sub_auxiliaryUnaryProbability_sub_failure_le_reject {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

An errorless MINKT heuristic rejects mass at least one minus the exact MINKT mass and its failure mass on every auxiliary-unary slice.

theorem Complexity.MINKT.auxiliaryUnary_rejectProbability_ge_average {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

The sharp incompressibility average gives an explicit lower bound on the correct rejection mass of every errorless MINKT heuristic.

theorem Complexity.MINKT.auxiliaryUnary_rejectProbability_ge_of_pointwise {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

If every split's low-complexity density is at most low and the heuristic fails with probability at most failure, then it correctly rejects mass at least 1 - low - failure.