Random-access conditional Kolmogorov complexity -- definitions

This layer fixes an explicit convention for C(x | y): an oracle machine gets Boolean random access to the finite condition y. Queries are canonical pairs of a one-bit tag and a minimal binary index. Tag false reads a data bit; tag true asks whether the index is in bounds. The second query form makes the condition length observable and prevents strings differing only by trailing zeroes from defining the same oracle.

Every oracle lookup costs one OracleTM step. Constructing and positioning a query on the query tape costs ordinary local steps.

def Complexity.RandomAccessCondition.bitQuery (index : ℕ) : List Bool

Canonical query for one condition bit.

Equations

• Complexity.RandomAccessCondition.bitQuery index = Complexity.pair [false] (Complexity.BinaryNatCode.encode index)

def Complexity.RandomAccessCondition.inBoundsQuery (index : ℕ) : List Bool

Canonical query asking whether index is below the condition length.

Equations

• Complexity.RandomAccessCondition.inBoundsQuery index = Complexity.pair [true] (Complexity.BinaryNatCode.encode index)

def Complexity.RandomAccessCondition.oracle (condition : List Bool) : BooleanOracle

Faithful Boolean random-access oracle for one finite condition string. Malformed query pairs, non-singleton tags, noncanonical indices, and out-of-range bit queries all return false.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.OracleTM.randomAccessConditionalPlainKolmogorovComplexity {n : ℕ} (machine : OracleTM n) (output condition : List Bool) : WithTop ℕ

Plain machine-relative conditional complexity when the finite condition is available through RandomAccessCondition.oracle.

Equations

• machine.randomAccessConditionalPlainKolmogorovComplexity output condition = machine.plainKolmogorovComplexity (Complexity.RandomAccessCondition.oracle condition) output

noncomputable def Complexity.OracleTM.randomAccessConditionalTimeBoundedKolmogorovComplexity {n : ℕ} (machine : OracleTM n) (output condition : List Bool) (time : ℕ) : WithTop ℕ

Whole-output time-bounded conditional complexity under the explicit random-access condition convention.

Equations

• machine.randomAccessConditionalTimeBoundedKolmogorovComplexity output condition time = machine.timeBoundedKolmogorovComplexity (Complexity.RandomAccessCondition.oracle condition) output time