Minimum time-bounded Kolmogorov complexity -- proof internals

Proofs of canonical-code exactness, short-program semantics, and monotonicity for the public MINKT API.

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

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

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

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

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

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

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

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

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

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

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

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