Machine-relative Kolmogorov complexity

This definitions layer introduces plain and time-bounded description complexity for every deterministic machine. Universality is deliberately not a precondition: it is relevant to invariance and upper bounds, not to the minimum itself. Extended naturals distinguish a genuine zero-length description from the absence of any description.

Prefix-free complexity is restricted to a machine carrying a proof that its halting domain is prefix-free. The library's ordinary input convention does not provide that property automatically.

Main definitions

• TM.plainKolmogorovComplexity -- machine-relative plain complexity C_U
• TM.timeBoundedKolmogorovComplexity -- whole-output bounded complexity C_U^t
• TM.HasPrefixFreeDomain -- prefix-freeness of the raw halting domain
• TM.PrefixFreeMachine -- a machine bundled with that domain certificate
• TM.prefixKolmogorovComplexity -- prefix-free complexity K_U

def Complexity.TM.producingProgramSizes {n : ℕ} (machine : TM n) (output : List Bool) : Set ℕ

Lengths of programs on which machine eventually produces output.

Equations

• machine.producingProgramSizes output = {size : ℕ | ∃ (program : List Bool), program.length = size ∧ machine.Produces program output}

def Complexity.TM.timeBoundedProducingProgramSizes {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) : Set ℕ

Lengths of programs on which machine produces output within time.

Equations

• machine.timeBoundedProducingProgramSizes output time = {size : ℕ | ∃ (program : List Bool), program.length = size ∧ machine.ProducesInTime program output time}

noncomputable def Complexity.TM.plainKolmogorovComplexity {n : ℕ} (machine : TM n) (output : List Bool) : WithTop ℕ

Plain machine-relative Kolmogorov complexity. The value is ⊤ exactly when no program makes machine produce output.

Equations

• machine.plainKolmogorovComplexity output = sInf ((fun (size : ℕ) => ↑size) '' machine.producingProgramSizes output)

noncomputable def Complexity.TM.timeBoundedKolmogorovComplexity {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) : WithTop ℕ

Whole-output time-bounded machine-relative Kolmogorov complexity. The primitive clock is explicit, and the value is ⊤ if no program produces the output within it.

Equations

• machine.timeBoundedKolmogorovComplexity output time = sInf ((fun (size : ℕ) => ↑size) '' machine.timeBoundedProducingProgramSizes output time)

def Complexity.TM.HasPrefixFreeDomain {n : ℕ} (machine : TM n) : Prop

The raw halting domain of machine is prefix-free: two halting programs related by the list-prefix order must be equal.

Equations

• machine.HasPrefixFreeDomain = ∀ {first second : List Bool}, machine.Halts first → machine.Halts second → first <+: second → first = second

structure Complexity.TM.PrefixFreeMachine (n : ℕ) : Type 1

A deterministic machine bundled with a proof that its halting domain is prefix-free. This certificate is what licenses K_U terminology.

• machine : TM n

  The underlying deterministic machine.

• prefixFree : self.machine.HasPrefixFreeDomain

  Its raw halting domain is prefix-free.

noncomputable def Complexity.TM.prefixKolmogorovComplexity {n : ℕ} (machine : PrefixFreeMachine n) (output : List Bool) : WithTop ℕ

Prefix-free Kolmogorov complexity for a certified prefix-free machine.

Equations

• Complexity.TM.prefixKolmogorovComplexity machine output = machine.machine.plainKolmogorovComplexity output