Minimum conditional time-bounded Kolmogorov complexity -- definitions

This layer fixes a canonical representation of a conditional description- complexity instance (x, y, 1^t). The output x is measured relative to the faithful random-access condition oracle for y; the primitive clock is encoded in unary.

The machine remains explicit. Universality and equivalence with another conditional-input convention are later hypotheses, not properties hidden in the definition.

structure Complexity.MINCKT.Instance : Type

A decoded conditional MinKT instance (x, y, 1^t).

• output : List Bool

  String whose conditional description complexity is measured.

• condition : List Bool

  Finite random-access condition.

• time : ℕ

  Primitive oracle-machine step budget, encoded in unary.

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

The canonical unary representation of the primitive clock.

Equations

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

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

Canonical right-associated encoding of (x, y, 1^t).

Equations

• inst.encode = Complexity.pair inst.output (Complexity.pair inst.condition inst.unaryClock)

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

Decode exactly one canonical output/condition/unary-clock triple.

Malformed outer or inner pairing and clocks containing false are rejected.

Equations

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

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

Replace only the primitive time bound.

Equations

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

noncomputable def Complexity.MINCKT.Instance.complexity {tapes : ℕ} (inst : Instance) (machine : OracleTM tapes) : WithTop ℕ

Machine-relative conditional complexity of the decoded instance.

Equations

• inst.complexity machine = machine.randomAccessConditionalTimeBoundedKolmogorovComplexity inst.output inst.condition inst.time

def Complexity.MINCKT.Instance.IsAtMost {tapes : ℕ} (inst : Instance) (machine : OracleTM tapes) (threshold : ℕ) : Prop

The bounded conditional complexity is at most an explicit threshold.

Equations

• inst.IsAtMost machine threshold = (inst.complexity machine ≤ ↑threshold)

def Complexity.MINCKT.Instance.HasProgramAtMost {tapes : ℕ} (inst : Instance) (machine : OracleTM tapes) (threshold : ℕ) : Prop

Direct program formulation of IsAtMost.

Equations

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