Machine-relative Kolmogorov complexity

Plain and whole-output time-bounded description complexity are defined for every deterministic machine, independently of universality. Both take values in WithTop ℕ, so ⊤ records that no qualifying program exists. Prefix-free complexity is exposed only for a machine whose raw halting domain is certified prefix-free.

The threshold theorems characterize each minimum by a short producing program. Generic simulations yield additive plain-complexity comparison, while a polynomial timed simulation gives an explicit resource-aware bounded-complexity comparison. Bounded input locality also implies that every finite t-time complexity value is at most t.

Main results

• TM.plainKolmogorovComplexity_le_coe_iff -- plain threshold characterization
• TM.timeBoundedKolmogorovComplexity_le_coe_iff -- bounded characterization
• TM.timeBoundedKolmogorovComplexity_lt_coe_iff -- strict characterization
• TM.timeBoundedKolmogorovComplexity_mono -- more time cannot increase complexity
• TM.timeBoundedKolmogorovComplexity_le_time -- finite values are at most the clock
• TM.computationalDepth_add_plain -- exact decomposition of bounded complexity
• TM.computationalDepth_mono -- more time cannot increase computational depth
• TM.computationalDepthBetween_add -- exact three-clock depth telescoping
• timeBoundedKolmogorovComplexity_pair_le_of_composition -- finite upper chain rule
• timeBoundedKolmogorovComplexity_pair_le_add_of_conditional_composition -- additive chain
• TimeBoundedSymmetryOfInformation -- explicit non-vacuous lower-chain hypothesis
• TimeBoundedSymmetryOfInformation.conditional_le_of_pair_upper -- depth-loss bridge
• TimeBoundedSymmetryOfInformation.conditional_le_of_composition -- evaluator bridge
• TM.Simulates.plainKolmogorovComplexity_le_add -- additive invariance direction
• TM.PolynomialTimeOverhead.kolmogorov_transfer -- resource-aware comparison
• TM.IsUniversal.plainKolmogorovComplexity_ne_top -- universal descriptions exist
• TM.IsEfficientlyUniversal.timeBoundedKolmogorovComplexity_printer -- uniform printer

@[simp]

theorem Complexity.TM.prefixKolmogorovComplexity_eq {n : ℕ} (machine : PrefixFreeMachine n) (output : List Bool) : prefixKolmogorovComplexity machine output = machine.machine.plainKolmogorovComplexity output

Prefix-free complexity is the plain minimum of the certified machine; the bundle's domain proof licenses the prefix-free interpretation.

theorem Complexity.TM.plainKolmogorovComplexity_le {n : ℕ} {machine : TM n} {program output : List Bool} (hproduce : machine.Produces program output) : machine.plainKolmogorovComplexity output ≤ ↑program.length

Any producing program upper-bounds plain complexity.

theorem Complexity.TM.plainKolmogorovComplexity_eq_top_iff {n : ℕ} (machine : TM n) (output : List Bool) : machine.plainKolmogorovComplexity output = ⊤ ↔ ¬∃ (program : List Bool), machine.Produces program output

Plain complexity is infinite exactly when the output has no description.

theorem Complexity.TM.plainKolmogorovComplexity_witness {n : ℕ} (machine : TM n) (output : List Bool) (hfinite : machine.plainKolmogorovComplexity output ≠ ⊤) : ∃ (program : List Bool), ↑program.length = machine.plainKolmogorovComplexity output ∧ machine.Produces program output

Every finite plain complexity value is attained by a producing program.

theorem Complexity.TM.plainKolmogorovComplexity_le_coe_iff {n : ℕ} (machine : TM n) (output : List Bool) (bound : ℕ) : machine.plainKolmogorovComplexity output ≤ ↑bound ↔ ∃ (program : List Bool), program.length ≤ bound ∧ machine.Produces program output

Plain complexity is at most bound exactly when a producing program of length at most bound exists.

theorem Complexity.TM.timeBoundedKolmogorovComplexity_le {n : ℕ} {machine : TM n} {program output : List Bool} {time : ℕ} (hproduce : machine.ProducesInTime program output time) : machine.timeBoundedKolmogorovComplexity output time ≤ ↑program.length

Any program producing within a clock upper-bounds time-bounded complexity.

theorem Complexity.TM.timeBoundedKolmogorovComplexity_eq_top_iff {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) : machine.timeBoundedKolmogorovComplexity output time = ⊤ ↔ ¬∃ (program : List Bool), machine.ProducesInTime program output time

Time-bounded complexity is infinite exactly when no program produces the output within the clock.

theorem Complexity.TM.timeBoundedKolmogorovComplexity_witness {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) (hfinite : machine.timeBoundedKolmogorovComplexity output time ≠ ⊤) : ∃ (program : List Bool), ↑program.length = machine.timeBoundedKolmogorovComplexity output time ∧ machine.ProducesInTime program output time

Every finite time-bounded complexity value is attained.

theorem Complexity.TM.timeBoundedKolmogorovComplexity_le_time {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) (hfinite : machine.timeBoundedKolmogorovComplexity output time ≠ ⊤) : machine.timeBoundedKolmogorovComplexity output time ≤ ↑time

Every finite t-time description complexity is at most t: a producing program can be truncated to the prefix reachable by the input head.

theorem Complexity.TM.timeBoundedKolmogorovComplexity_le_coe_iff {n : ℕ} (machine : TM n) (output : List Bool) (time bound : ℕ) : machine.timeBoundedKolmogorovComplexity output time ≤ ↑bound ↔ ∃ (program : List Bool), program.length ≤ bound ∧ machine.ProducesInTime program output time

Time-bounded complexity is at most bound exactly when a short program produces the output within the clock.

theorem Complexity.TM.timeBoundedKolmogorovComplexity_lt_coe_iff {n : ℕ} (machine : TM n) (output : List Bool) (time bound : ℕ) : machine.timeBoundedKolmogorovComplexity output time < ↑bound ↔ ∃ (program : List Bool), program.length < bound ∧ machine.ProducesInTime program output time

Time-bounded complexity is strictly below bound exactly when a program strictly shorter than bound produces the output within the clock.

theorem Complexity.TM.timeBoundedKolmogorovComplexity_mono {n : ℕ} (machine : TM n) (output : List Bool) {first second : ℕ} (hclock : first ≤ second) : machine.timeBoundedKolmogorovComplexity output second ≤ machine.timeBoundedKolmogorovComplexity output first

Enlarging the clock cannot increase time-bounded complexity.

theorem Complexity.TM.plainKolmogorovComplexity_le_timeBounded {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) : machine.plainKolmogorovComplexity output ≤ machine.timeBoundedKolmogorovComplexity output time

Removing the time restriction cannot increase description complexity.

theorem Complexity.TM.Simulates.plainKolmogorovComplexity_le_add {simulatorTapes sourceTapes : ℕ} {simulator : TM simulatorTapes} {source : TM sourceTapes} {compile : List Bool → List Bool} {constant : ℕ} (hsim : simulator.Simulates source compile) (hlength : HasAdditiveProgramOverhead compile constant) (output : List Bool) : simulator.plainKolmogorovComplexity output ≤ source.plainKolmogorovComplexity output + ↑constant

An output-preserving compiler with additive length overhead gives the corresponding direction of the plain Kolmogorov invariance inequality.

theorem Complexity.TM.PolynomialTimeOverhead.kolmogorov_transfer {simulatorTapes sourceTapes : ℕ} {simulator : TM simulatorTapes} {source : TM sourceTapes} {compile : List Bool → List Bool} {constant : ℕ} {clock : TimeOverhead} (hsim : simulator.SimulatesInTime source compile clock) (hlength : HasAdditiveProgramOverhead compile constant) (hclock : PolynomialTimeOverhead clock) : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (output : List Bool) (sourceTime bound : ℕ), source.timeBoundedKolmogorovComplexity output sourceTime ≤ ↑bound → simulator.timeBoundedKolmogorovComplexity output (coefficient * (bound + sourceTime + 1) ^ exponent) ≤ ↑(bound + constant)

A polynomial timed simulation transfers a bounded description of length bound into one of length bound + constant under an explicit polynomially larger clock. The returned coefficients are those supplied by the clock policy.

theorem Complexity.TM.IsUniversal.plainKolmogorovComplexity_ne_top {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsUniversal) (output : List Bool) : simulator.plainKolmogorovComplexity output ≠ ⊤

Every semantically universal machine has a finite plain description of every binary string. The proof uses universality only against the fixed input-to-output copy machine.

theorem Complexity.TM.IsUniversal.exists_timeBoundedKolmogorovComplexity_ne_top {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsUniversal) (output : List Bool) : ∃ (time : ℕ), simulator.timeBoundedKolmogorovComplexity output time ≠ ⊤

Every output has finite bounded complexity at some clock on any semantically universal machine. Semantic universality alone does not select a uniform time bound.

theorem Complexity.TM.IsEfficientlyUniversal.timeBoundedKolmogorovComplexity_printer {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsEfficientlyUniversal) : ∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ), ∀ (output : List Bool) (time : ℕ), coefficient * (2 * output.length + 3) ^ exponent ≤ time → simulator.timeBoundedKolmogorovComplexity output time ≤ ↑(output.length + constant)

Polynomially efficient universality supplies one uniform printer: every string x has a description of length at most |x| + constant within coefficient * (2|x| + 3)^exponent steps. The same bound remains valid at every larger clock.

theorem Complexity.TM.IsEfficientlyUniversal.plainKolmogorovComplexity_le_length_add {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsEfficientlyUniversal) : ∃ (constant : ℕ), ∀ (output : List Bool), simulator.plainKolmogorovComplexity output ≤ ↑(output.length + constant)

Efficient universality gives the usual linear self-description upper bound for plain complexity, with one additive constant for every output.

theorem Complexity.TM.IsEfficientlyUniversal.exists_polynomial_printer_finite {simulatorTapes : ℕ} {simulator : TM simulatorTapes} (huniversal : simulator.IsEfficientlyUniversal) : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (output : List Bool), simulator.timeBoundedKolmogorovComplexity output (coefficient * (2 * output.length + 3) ^ exponent) ≠ ⊤

The uniform polynomial printer clock makes time-bounded complexity finite for every output of an efficiently universal machine.