Machine-relative Kolmogorov complexity -- proof internals

Proofs supporting the public API in Complexitylib.Metacomplexity.Kolmogorov.

theorem Complexity.TM.plainKolmogorovComplexity_le_internal {n : ℕ} {machine : TM n} {program output : List Bool} (hproduce : machine.Produces program output) : machine.plainKolmogorovComplexity output ≤ ↑program.length

theorem Complexity.TM.plainKolmogorovComplexity_eq_top_iff_internal {n : ℕ} (machine : TM n) (output : List Bool) : machine.plainKolmogorovComplexity output = ⊤ ↔ ¬∃ (program : List Bool), machine.Produces program output

theorem Complexity.TM.plainKolmogorovComplexity_witness_internal {n : ℕ} (machine : TM n) (output : List Bool) (hfinite : machine.plainKolmogorovComplexity output ≠ ⊤) : ∃ (program : List Bool), ↑program.length = machine.plainKolmogorovComplexity output ∧ machine.Produces program output

theorem Complexity.TM.plainKolmogorovComplexity_le_coe_iff_internal {n : ℕ} (machine : TM n) (output : List Bool) (bound : ℕ) : machine.plainKolmogorovComplexity output ≤ ↑bound ↔ ∃ (program : List Bool), program.length ≤ bound ∧ machine.Produces program output

theorem Complexity.TM.timeBoundedKolmogorovComplexity_le_internal {n : ℕ} {machine : TM n} {program output : List Bool} {time : ℕ} (hproduce : machine.ProducesInTime program output time) : machine.timeBoundedKolmogorovComplexity output time ≤ ↑program.length

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

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

theorem Complexity.TM.timeBoundedKolmogorovComplexity_le_time_internal {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) (hfinite : machine.timeBoundedKolmogorovComplexity output time ≠ ⊤) : machine.timeBoundedKolmogorovComplexity output time ≤ ↑time

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

theorem Complexity.TM.timeBoundedKolmogorovComplexity_lt_coe_iff_internal {n : ℕ} (machine : TM n) (output : List Bool) (time bound : ℕ) : machine.timeBoundedKolmogorovComplexity output time < ↑bound ↔ ∃ (program : List Bool), program.length < bound ∧ machine.ProducesInTime program output time

theorem Complexity.TM.timeBoundedKolmogorovComplexity_mono_internal {n : ℕ} (machine : TM n) (output : List Bool) {first second : ℕ} (hclock : first ≤ second) : machine.timeBoundedKolmogorovComplexity output second ≤ machine.timeBoundedKolmogorovComplexity output first

theorem Complexity.TM.plainKolmogorovComplexity_le_timeBounded_internal {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) : machine.plainKolmogorovComplexity output ≤ machine.timeBoundedKolmogorovComplexity output time

theorem Complexity.TM.simulates_plainKolmogorovComplexity_le_add_internal {simulatorTapes sourceTapes : ℕ} {simulator : TM simulatorTapes} {source : TM sourceTapes} {compile : List Bool → List Bool} {constant : ℕ} (hsim : simulator.Simulates source compile) (hlength : HasAdditiveProgramOverhead compile constant) (output : List Bool) : simulator.plainKolmogorovComplexity output ≤ source.plainKolmogorovComplexity output + ↑constant

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

theorem Complexity.TM.IsUniversal.plainKolmogorovComplexity_ne_top_internal {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsUniversal) (output : List Bool) : simulator.plainKolmogorovComplexity output ≠ ⊤

theorem Complexity.TM.IsUniversal.exists_timeBoundedKolmogorovComplexity_ne_top_internal {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsUniversal) (output : List Bool) : ∃ (time : ℕ), simulator.timeBoundedKolmogorovComplexity output time ≠ ⊤

theorem Complexity.TM.IsEfficientlyUniversal.timeBoundedKolmogorovComplexity_printer_internal {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsEfficientlyUniversal) : ∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ), ∀ (output : List Bool) (time : ℕ), coefficient * (2 * output.length + 3) ^ exponent ≤ time → simulator.timeBoundedKolmogorovComplexity output time ≤ ↑(output.length + constant)

theorem Complexity.TM.IsEfficientlyUniversal.plainKolmogorovComplexity_le_length_add_internal {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsEfficientlyUniversal) : ∃ (constant : ℕ), ∀ (output : List Bool), simulator.plainKolmogorovComplexity output ≤ ↑(output.length + constant)

theorem Complexity.TM.IsEfficientlyUniversal.exists_polynomial_printer_finite_internal {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsEfficientlyUniversal) : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (output : List Bool), simulator.timeBoundedKolmogorovComplexity output (coefficient * (2 * output.length + 3) ^ exponent) ≠ ⊤