Random-access conditional Kolmogorov complexity -- proof internals

theorem Complexity.RandomAccessCondition.oracle_bitQuery_internal (condition : List Bool) (index : ℕ) : oracle condition (bitQuery index) = condition[index]?.getD false

theorem Complexity.RandomAccessCondition.oracle_inBoundsQuery_internal (condition : List Bool) (index : ℕ) : oracle condition (inBoundsQuery index) = decide (index < condition.length)

theorem Complexity.RandomAccessCondition.oracle_injective_internal : Function.Injective oracle

theorem Complexity.OracleTM.randomAccessConditionalPlainKolmogorovComplexity_le_internal {n : ℕ} {machine : OracleTM n} {program output condition : List Bool} (hproduce : machine.Produces (RandomAccessCondition.oracle condition) program output) : machine.randomAccessConditionalPlainKolmogorovComplexity output condition ≤ ↑program.length

theorem Complexity.OracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity_le_internal {n : ℕ} {machine : OracleTM n} {program output condition : List Bool} {time : ℕ} (hproduce : machine.ProducesInTime (RandomAccessCondition.oracle condition) program output time) : machine.randomAccessConditionalTimeBoundedKolmogorovComplexity output condition time ≤ ↑program.length

theorem Complexity.OracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity_eq_top_iff_internal {n : ℕ} (machine : OracleTM n) (output condition : List Bool) (time : ℕ) : machine.randomAccessConditionalTimeBoundedKolmogorovComplexity output condition time = ⊤ ↔ ¬∃ (program : List Bool), machine.ProducesInTime (RandomAccessCondition.oracle condition) program output time

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

theorem Complexity.OracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity_le_coe_iff_internal {n : ℕ} (machine : OracleTM n) (output condition : List Bool) (time bound : ℕ) : machine.randomAccessConditionalTimeBoundedKolmogorovComplexity output condition time ≤ ↑bound ↔ ∃ (program : List Bool), program.length ≤ bound ∧ machine.ProducesInTime (RandomAccessCondition.oracle condition) program output time

theorem Complexity.OracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity_mono_internal {n : ℕ} (machine : OracleTM n) (output condition : List Bool) {first second : ℕ} (hclock : first ≤ second) : machine.randomAccessConditionalTimeBoundedKolmogorovComplexity output condition second ≤ machine.randomAccessConditionalTimeBoundedKolmogorovComplexity output condition first

theorem Complexity.OracleTM.SimulatesInTime.randomAccessConditionalKolmogorov_transfer_internal {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 : ℕ), ∀ (condition output : List Bool) (sourceTime bound : ℕ), source.randomAccessConditionalTimeBoundedKolmogorovComplexity output condition sourceTime ≤ ↑bound → simulator.randomAccessConditionalTimeBoundedKolmogorovComplexity output condition (coefficient * (bound + sourceTime + 1) ^ exponent) ≤ ↑(bound + constant)

theorem Complexity.TM.toOracleTM_randomAccessConditionalTimeBoundedKolmogorovComplexity_eq_internal {n : ℕ} (machine : TM n) (output condition : List Bool) (time : ℕ) : machine.toOracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity output condition time = machine.timeBoundedKolmogorovComplexity output time