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 machine-relative 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 coefficient and exponent are uniform over all outputs, source clocks and bounds. (The proof takes them from the clock policy hclock, but the statement asserts only their existence.)

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.