Oracle-relative Kolmogorov complexity

This module exposes plain and time-bounded description complexity relative to an arbitrary deterministic oracle machine and Boolean oracle. The ordinary TM embedding preserves bounded complexity exactly for every oracle. An oracle-uniform polynomial simulation transfers bounded descriptions with one compiler constant and clock shared by all oracles.

theorem Complexity.OracleTM.plainKolmogorovComplexity_le {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {program output : List Bool} (hproduce : machine.Produces oracle program output) : machine.plainKolmogorovComplexity oracle output ≤ ↑program.length

Any oracle program producing the requested output upper-bounds plain oracle-relative complexity.

theorem Complexity.OracleTM.timeBoundedKolmogorovComplexity_le {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {program output : List Bool} {time : ℕ} (hproduce : machine.ProducesInTime oracle program output time) : machine.timeBoundedKolmogorovComplexity oracle output time ≤ ↑program.length

Any oracle program producing within a clock upper-bounds time-bounded oracle-relative complexity.

theorem Complexity.OracleTM.timeBoundedKolmogorovComplexity_eq_top_iff {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (output : List Bool) (time : ℕ) : machine.timeBoundedKolmogorovComplexity oracle output time = ⊤ ↔ ¬∃ (program : List Bool), machine.ProducesInTime oracle program output time

Bounded oracle complexity is infinite exactly when no program produces the output within the clock.

theorem Complexity.OracleTM.timeBoundedKolmogorovComplexity_witness {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (output : List Bool) (time : ℕ) (hfinite : machine.timeBoundedKolmogorovComplexity oracle output time ≠ ⊤) : ∃ (program : List Bool), ↑program.length = machine.timeBoundedKolmogorovComplexity oracle output time ∧ machine.ProducesInTime oracle program output time

Every finite bounded oracle complexity value is attained by a program.

theorem Complexity.OracleTM.timeBoundedKolmogorovComplexity_le_coe_iff {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (output : List Bool) (time bound : ℕ) : machine.timeBoundedKolmogorovComplexity oracle output time ≤ ↑bound ↔ ∃ (program : List Bool), program.length ≤ bound ∧ machine.ProducesInTime oracle program output time

Bounded oracle complexity is at most bound exactly when a program of at most that length produces the output within the clock.

theorem Complexity.OracleTM.timeBoundedKolmogorovComplexity_mono {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (output : List Bool) {first second : ℕ} (hclock : first ≤ second) : machine.timeBoundedKolmogorovComplexity oracle output second ≤ machine.timeBoundedKolmogorovComplexity oracle output first

Enlarging the oracle-machine clock cannot increase bounded complexity.

theorem Complexity.OracleTM.SimulatesInTime.kolmogorov_transfer {simulatorTapes sourceTapes : ℕ} {simulator : OracleTM simulatorTapes} {source : OracleTM sourceTapes} {compile : List Bool → List Bool} {constant : ℕ} {clock : TM.TimeOverhead} (hsim : simulator.SimulatesInTime source compile clock) (hlength : TM.HasAdditiveProgramOverhead compile constant) (hclock : TM.PolynomialTimeOverhead clock) : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (oracle : BooleanOracle) (output : List Bool) (sourceTime bound : ℕ), source.timeBoundedKolmogorovComplexity oracle output sourceTime ≤ ↑bound → simulator.timeBoundedKolmogorovComplexity oracle output (coefficient * (bound + sourceTime + 1) ^ exponent) ≤ ↑(bound + constant)

An oracle-uniform polynomial simulation transfers every bounded oracle-relative description using the same compiler constant and polynomial clock for all Boolean oracles.

theorem Complexity.TM.toOracleTM_timeBoundedKolmogorovComplexity_eq {n : ℕ} (machine : TM n) (oracle : BooleanOracle) (output : List Bool) (time : ℕ) : machine.toOracleTM.timeBoundedKolmogorovComplexity oracle output time = machine.timeBoundedKolmogorovComplexity output time

Embedding an ordinary machine into the oracle model preserves its bounded Kolmogorov complexity exactly, independently of the supplied oracle.