Documentation

Complexitylib.Metacomplexity.MINCKT

Minimum conditional time-bounded Kolmogorov complexity #

This module exposes canonical (x, y, 1^t) instances for machine-relative conditional time-bounded Kolmogorov complexity. Conditions use the library's faithful random-access oracle convention. Universality and paper-specific evaluator equivalence remain explicit future obligations. The depth-adjusted GapMINCKT promise follows Hirahara's 2022 Definition 6.1.

source
@[simp]
theorem Complexity.MINCKT.Instance.length_unaryClock (inst : Instance) :
inst.unaryClock.length = inst.time

The unary clock has exactly the represented length.

source
@[simp]
theorem Complexity.MINCKT.Instance.decode?_encode (inst : Instance) :
decode? inst.encode = some inst

Every canonical conditional MinKT instance decodes exactly.

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

Successful decoding characterizes canonical instance encodings.

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

Decoding fails exactly on noncanonical strings.

source
theorem Complexity.MINCKT.Instance.encode_injective :
Function.Injective encode

Canonical conditional MinKT encoding is injective.

source
@[simp]
theorem Complexity.MINCKT.Instance.length_encode (inst : Instance) :
inst.encode.length = 2 * inst.output.length + 2 * inst.condition.length + inst.time + 4

Exact code length for the right-associated tuple (x, y, 1^t).

source
theorem Complexity.MINCKT.Instance.isAtMost_iff_hasProgramAtMost {tapes : ℕ} (inst : Instance) (machine : OracleTM tapes) (threshold : ℕ) :
inst.IsAtMost machine threshold ↔ inst.HasProgramAtMost machine threshold

A conditional complexity threshold is equivalent to a direct bounded program witness.

source
theorem Complexity.MINCKT.Instance.IsAtMost.withTime_mono {tapes : ℕ} (inst : Instance) (machine : OracleTM tapes) (threshold : ℕ) {first second : ℕ} (hclock : first ≤ second) (hsmall : (inst.withTime first).IsAtMost machine threshold) :
(inst.withTime second).IsAtMost machine threshold

Giving the conditional evaluator more time preserves an upper threshold.

source
theorem Complexity.MINCKT.Instance.IsAtMost.threshold_mono {tapes : ℕ} (inst : Instance) (machine : OracleTM tapes) {first second : ℕ} (hthreshold : first ≤ second) (hsmall : inst.IsAtMost machine first) :
inst.IsAtMost machine second

Increasing the description threshold preserves membership.