Random-access conditional Kolmogorov complexity

The finite condition is exposed through a faithful Boolean oracle. Canonical tagged queries separately read condition bits and test whether an index is in bounds, so the oracle retains both contents and length. This is an explicit random-access convention suitable for conditional meta-complexity; any theorem whose source fixes a different evaluator convention must provide a simulation bridge rather than identify the models silently.

@[simp]

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

A canonical bit query returns the indexed bit, defaulting to false out of bounds.

@[simp]

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

A canonical bounds query says exactly whether the index is valid.

theorem Complexity.RandomAccessCondition.oracle_injective : Function.Injective oracle

The random-access oracle faithfully retains the finite condition, including its length.

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

Any program producing relative to the condition oracle upper-bounds plain conditional complexity.

theorem Complexity.OracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity_le {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

Any program producing within the clock upper-bounds bounded conditional complexity.

theorem Complexity.OracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity_eq_top_iff {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

Bounded conditional complexity is infinite exactly when no program produces relative to the condition oracle within the clock.

theorem Complexity.OracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity_witness {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

Every finite bounded conditional complexity value is attained.

theorem Complexity.OracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity_le_coe_iff {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

Bounded conditional complexity is at most bound exactly when a program of at most that length succeeds within the clock.

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

Enlarging the clock cannot increase bounded conditional complexity.

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

An oracle-uniform polynomial simulation transfers conditional descriptions with one compiler constant and clock shared by every finite condition.

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

An embedded ordinary machine ignores every condition, so its bounded conditional complexity is exactly its ordinary bounded complexity.