The Minimum Time-Bounded Kolmogorov Complexity problem

This module exposes a canonical, total machine-relative MINKT[r] language. Its inputs are encoded as (x, 1^t), and its strict threshold convention is

C_U^t(x) < r(|x|).

Universality is deliberately separate: all definitions and finite facts hold for an arbitrary deterministic machine, while later invariance and hardness results can ask for the precise efficient-universality property they use.

Main definitions

• MINKT.Instance -- an output string and primitive unary clock
• MINKT.Instance.encode / decode? -- canonical total codec
• MINKT.Instance.IsBelow -- strict time-bounded complexity predicate
• MINKT.ProgramWitnessRelation -- direct short-program witness relation
• MINKT -- encoded language, with malformed strings rejected
• GapMINKT.Logarithmic.problem -- exact s + log_2(tau) promise

@[simp]

theorem Complexity.MINKT.Instance.length_unaryClock (inst : Instance) : inst.unaryClock.length = inst.time

The unary clock contains exactly time bits.

@[simp]

theorem Complexity.MINKT.Instance.decode?_encode (inst : Instance) : decode? inst.encode = some inst

Canonical MINKT encodings decode to their original instances.

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

Exact decoding accepts precisely canonical output/unary-clock encodings.

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

Decoding rejects exactly the noncanonical strings.

theorem Complexity.MINKT.Instance.encode_injective : Function.Injective encode

Canonical MINKT encoding is injective.

@[simp]

theorem Complexity.MINKT.Instance.length_encode (inst : Instance) : inst.encode.length = 2 * inst.output.length + 2 + inst.time

Exact encoded length: a doubled self-delimiting output followed by the unary clock.

theorem Complexity.MINKT.Instance.isBelow_iff_hasProgramShorterThan {tapes : ℕ} (inst : Instance) (machine : TM tapes) (threshold : ℕ → ℕ) : inst.IsBelow machine threshold ↔ inst.HasProgramShorterThan machine threshold

Strict time-bounded complexity is equivalent to a producing program whose length is strictly below the length-dependent threshold.

theorem Complexity.MINKT.Instance.IsBelow.withTime_mono {tapes : ℕ} (inst : Instance) (machine : TM tapes) (threshold : ℕ → ℕ) {first second : ℕ} (hclock : first ≤ second) (hsmall : (inst.withTime first).IsBelow machine threshold) : (inst.withTime second).IsBelow machine threshold

Increasing an instance's clock preserves a MINKT yes-instance.

theorem Complexity.MINKT.Instance.IsBelow.threshold_mono {tapes : ℕ} (inst : Instance) (machine : TM tapes) {first second : ℕ → ℕ} (hthreshold : ∀ (length : ℕ), first length ≤ second length) (hsmall : inst.IsBelow machine first) : inst.IsBelow machine second

Pointwise increasing the threshold preserves a MINKT yes-instance.

@[simp]

theorem Complexity.MINKT.mem_encode_iff {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (inst : Instance) : inst.encode ∈ MINKT machine threshold ↔ inst.IsBelow machine threshold

A canonical code belongs to MINKT[threshold] exactly when its instance satisfies the strict time-bounded complexity inequality.

theorem Complexity.MINKT.mem_encode_iff_exists_program {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (inst : Instance) : inst.encode ∈ MINKT machine threshold ↔ ∃ (program : List Bool), program.length < threshold inst.output.length ∧ machine.ProducesInTime program inst.output inst.time

Canonical membership has an exact direct short-program characterization.

theorem Complexity.MINKT.not_mem_of_decode?_eq_none {tapes : ℕ} {machine : TM tapes} {threshold : ℕ → ℕ} {bits : List Bool} (hdecode : Instance.decode? bits = none) : bits ∉ MINKT machine threshold

Every malformed instance code is rejected by the total MINKT language.

theorem Complexity.MINKT.mem_iff_exists_instance {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (bits : List Bool) : bits ∈ MINKT machine threshold ↔ ∃ (inst : Instance), Instance.decode? bits = some inst ∧ inst.IsBelow machine threshold

Decoded membership has an explicit unique-instance witness.

theorem Complexity.MINKT.mem_iff_exists_programWitness {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (bits : List Bool) : bits ∈ MINKT machine threshold ↔ ∃ (program : List Bool), ProgramWitnessRelation machine threshold bits program

MINKT membership is exactly existence of a raw short-program witness.

theorem Complexity.MINKT.programWitnessRelation_length_le_polynomial {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (polynomial : Polynomial ℕ) (hthreshold : ∀ (length : ℕ), threshold length ≤ Polynomial.eval length polynomial) {bits program : List Bool} (hrelation : ProgramWitnessRelation machine threshold bits program) : program.length ≤ Polynomial.eval bits.length polynomial

A polynomial bound on the threshold gives the same polynomial bound on every accepted raw program witness, measured against the encoded input.

theorem Complexity.MINKT.programWitnessRelation_polyBalanced {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (hthreshold : PolyBound threshold) : PolyBalanced (ProgramWitnessRelation machine threshold)

If the MINKT threshold is polynomially bounded, its raw program relation is polynomially balanced.

theorem Complexity.MINKT.programWitnessRelation_mem_FNP_of_pairLang_mem_P {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (hthreshold : PolyBound threshold) (hverifier : pairLang (ProgramWitnessRelation machine threshold) ∈ P) : ProgramWitnessRelation machine threshold ∈ FNP

With polynomial threshold growth, a polynomial-time paired verifier makes the raw MINKT program relation an FNP relation.

theorem Complexity.MINKT.mem_NP_of_pairLang_mem_P {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (hthreshold : PolyBound threshold) (hverifier : pairLang (ProgramWitnessRelation machine threshold) ∈ P) : MINKT machine threshold ∈ NP

NP packaging for MINKT: polynomial threshold growth and a polynomial-time paired verifier suffice.

theorem Complexity.MINKT.mono {tapes : ℕ} (machine : TM tapes) {first second : ℕ → ℕ} (hthreshold : ∀ (length : ℕ), first length ≤ second length) : MINKT machine first ⊆ MINKT machine second

Pointwise threshold growth gives language inclusion.