Finite incompressibility -- definitions

This layer packages all binary programs of length at most a bound and the finite sets of fixed-length strings whose machine-relative time-bounded Kolmogorov complexity is below or above that bound.

@[reducible, inline]

abbrev Complexity.StrictShortProgram (bound : ℕ) : Type

A binary program of length strictly below bound.

Equations

• Complexity.StrictShortProgram bound = ((length : Fin bound) × (Fin ↑length → Bool))

def Complexity.StrictShortProgram.toList {bound : ℕ} (program : StrictShortProgram bound) : List Bool

Forget the strict length certificate and recover the variable-length program.

Equations

• program.toList = List.ofFn program.snd

def Complexity.StrictShortProgram.ofList (bound : ℕ) (program : List Bool) (hlength : program.length < bound) : StrictShortProgram bound

Package a variable-length program with a strict length certificate.

Equations

• Complexity.StrictShortProgram.ofList bound program hlength = ⟨⟨program.length, hlength⟩, program.get⟩

@[reducible, inline]

abbrev Complexity.ShortProgram (bound : ℕ) : Type

A binary program of length at most bound, represented by its length and fixed-length contents.

Equations

• Complexity.ShortProgram bound = ((length : Fin (bound + 1)) × (Fin ↑length → Bool))

def Complexity.ShortProgram.toList {bound : ℕ} (program : ShortProgram bound) : List Bool

Forget the length certificate and recover the variable-length program.

Equations

• program.toList = List.ofFn program.snd

def Complexity.ShortProgram.ofList (bound : ℕ) (program : List Bool) (hlength : program.length ≤ bound) : ShortProgram bound

Package a variable-length program with a proof that it meets the bound.

Equations

• Complexity.ShortProgram.ofList bound program hlength = ⟨⟨program.length, ⋯⟩, program.get⟩

noncomputable def Complexity.TM.timeBoundedStrictlyCompressibleStrings {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : Finset (Fin outputLength → Bool)

Fixed-length strings having a description strictly shorter than threshold within the specified clock. This is the exact low-complexity event used by strict-threshold MINKT.

Equations

• machine.timeBoundedStrictlyCompressibleStrings outputLength time threshold = {output : Fin outputLength → Bool | machine.timeBoundedKolmogorovComplexity (List.ofFn output) time < ↑threshold}

noncomputable def Complexity.TM.timeBoundedRandomStrings {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : Finset (Fin outputLength → Bool)

Fixed-length threshold-random strings, namely those whose time-bounded complexity is at least threshold.

Equations

• machine.timeBoundedRandomStrings outputLength time threshold = (machine.timeBoundedStrictlyCompressibleStrings outputLength time threshold)ᶜ

noncomputable def Complexity.TM.timeBoundedCompressibleStrings {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) : Finset (Fin outputLength → Bool)

Fixed-length strings having a description of length at most bound within the specified clock.

Equations

• machine.timeBoundedCompressibleStrings outputLength time bound = {output : Fin outputLength → Bool | machine.timeBoundedKolmogorovComplexity (List.ofFn output) time ≤ ↑bound}

noncomputable def Complexity.TM.timeBoundedIncompressibleStrings {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) : Finset (Fin outputLength → Bool)

Fixed-length strings whose time-bounded complexity exceeds bound.

Equations

• machine.timeBoundedIncompressibleStrings outputLength time bound = (machine.timeBoundedCompressibleStrings outputLength time bound)ᶜ