Minimum time-bounded Kolmogorov complexity -- definitions

This definitions layer gives MINKT[r] a total machine-relative semantics and a canonical auxiliary-unary input format. An instance is a pair (x, 1^t) of an output string and a unary clock. It is a yes-instance exactly when C_U^t(x) < r(|x|).

The comparison is intentionally strict. This matches the convention in which an r-random string satisfies C_U^t(x) >= r(|x|), so MINKT[r] recognizes the complementary low-complexity strings. The machine is an explicit parameter; universality is a hypothesis for machine-invariance or hardness theorems, not part of the minimum's definition.

The decoder accepts the empty unary clock as time zero, making the language total at every input. Auxiliary-unary distributions used in average-case results can separately restrict their sampled clock to be positive.

structure Complexity.MINKT.Instance : Type

A decoded MINKT instance consisting of an output and a unary time bound.

• output : List Bool

  String whose time-bounded description complexity is measured.

• time : ℕ

  Primitive machine-step budget, encoded in unary.

def Complexity.MINKT.Instance.unaryClock (inst : Instance) : List Bool

The canonical unary representation of the time bound.

Equations

• inst.unaryClock = List.replicate inst.time true

def Complexity.MINKT.Instance.encode (inst : Instance) : List Bool

Canonically encode an instance as the self-delimiting pair (x, 1^t).

Equations

• inst.encode = Complexity.pair inst.output inst.unaryClock

def Complexity.MINKT.Instance.decode? (bits : List Bool) : Option Instance

Decode exactly one canonical output/unary-clock pair.

Malformed pairing and clocks containing false are rejected.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.MINKT.Instance.withTime (inst : Instance) (time : ℕ) : Instance

Replace only the primitive time bound of an instance.

Equations

• inst.withTime time = { output := inst.output, time := time }

def Complexity.MINKT.Instance.IsBelow {tapes : ℕ} (inst : Instance) (machine : TM tapes) (threshold : ℕ → ℕ) : Prop

The strict machine-relative MINKT predicate C_U^t(x) < r(|x|).

Equations

• inst.IsBelow machine threshold = (machine.timeBoundedKolmogorovComplexity inst.output inst.time < ↑(threshold inst.output.length))

def Complexity.MINKT.Instance.HasProgramShorterThan {tapes : ℕ} (inst : Instance) (machine : TM tapes) (threshold : ℕ → ℕ) : Prop

Direct short-program formulation of the MINKT predicate.

Equations

• inst.HasProgramShorterThan machine threshold = ∃ (program : List Bool), program.length < threshold inst.output.length ∧ machine.ProducesInTime program inst.output inst.time

def Complexity.MINKT.ProgramWitnessRelation {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) (bits program : List Bool) : Prop

A raw witness relation for encoded MINKT instances.

The witness is the candidate short program. Canonical instance decoding, strict length, exact output, and the primitive clock are all retained.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.MINKT {tapes : ℕ} (machine : TM tapes) (threshold : ℕ → ℕ) : Language

The total strict-threshold Minimum Time-Bounded Kolmogorov Complexity language relative to machine and length threshold threshold.

Malformed codes are no-instances.

Equations

• Complexity.MINKT machine threshold = {bits : List Bool | match Complexity.MINKT.Instance.decode? bits with | some inst => inst.IsBelow machine threshold | none => False}