Computational depth

Machine-relative computational depth is formalized as C_M^time(output) - C_M(output). The extended-natural difference preserves ⊤ rather than totalizing a missing description as zero. The exact additive decomposition, finiteness criterion, clock monotonicity, and zero-depth characterization are proved before any symmetry-of-information hypothesis.

@[simp]

theorem Complexity.descriptionDifference_top_left (lower : WithTop ℕ) : descriptionDifference ⊤ lower = ⊤

Infinite upper description length gives infinite difference.

@[simp]

theorem Complexity.descriptionDifference_top_right (upper : WithTop ℕ) : descriptionDifference upper ⊤ = ⊤

Infinite lower description length gives infinite difference.

@[simp]

theorem Complexity.descriptionDifference_coe (upper lower : ℕ) : descriptionDifference ↑upper ↑lower = ↑(upper - lower)

On finite values, description difference is natural subtraction.

theorem Complexity.descriptionDifference_add_lower {upper lower : WithTop ℕ} (horder : lower ≤ upper) : descriptionDifference upper lower + lower = upper

If the lower description length is at most the upper one, their difference adds back to the upper length exactly.

theorem Complexity.descriptionDifference_eq_top_iff {upper lower : WithTop ℕ} (horder : lower ≤ upper) : descriptionDifference upper lower = ⊤ ↔ upper = ⊤

Under the same order, description difference is infinite exactly when its upper value is infinite.

theorem Complexity.descriptionDifference_eq_zero_iff {upper lower : WithTop ℕ} (horder : lower ≤ upper) (hfinite : upper ≠ ⊤) : descriptionDifference upper lower = 0 ↔ upper = lower

For a finite ordered pair, description difference vanishes exactly when the two lengths coincide.

theorem Complexity.descriptionDifference_add {upper middle lower : WithTop ℕ} (hlower : lower ≤ middle) (hupper : middle ≤ upper) : descriptionDifference upper middle + descriptionDifference middle lower = descriptionDifference upper lower

Description differences telescope through an ordered intermediate value.

theorem Complexity.TM.computationalDepthBetween_add_later {n : ℕ} (machine : TM n) (output : List Bool) {firstTime laterTime : ℕ} (hclock : firstTime ≤ laterTime) : machine.computationalDepthBetween output firstTime laterTime + machine.timeBoundedKolmogorovComplexity output laterTime = machine.timeBoundedKolmogorovComplexity output firstTime

Two-clock depth plus the later-clock complexity reconstructs the earlier- clock complexity exactly.

theorem Complexity.TM.computationalDepthBetween_le_first {n : ℕ} (machine : TM n) (output : List Bool) {firstTime laterTime : ℕ} (hclock : firstTime ≤ laterTime) : machine.computationalDepthBetween output firstTime laterTime ≤ machine.timeBoundedKolmogorovComplexity output firstTime

Two-clock depth never exceeds the earlier-clock complexity.

theorem Complexity.TM.computationalDepthBetween_eq_top_iff {n : ℕ} (machine : TM n) (output : List Bool) {firstTime laterTime : ℕ} (hclock : firstTime ≤ laterTime) : machine.computationalDepthBetween output firstTime laterTime = ⊤ ↔ machine.timeBoundedKolmogorovComplexity output firstTime = ⊤

Ordered two-clock depth is infinite exactly when the earlier-clock complexity is infinite.

theorem Complexity.TM.computationalDepthBetween_mono_first {n : ℕ} (machine : TM n) (output : List Bool) {firstTime secondTime laterTime : ℕ} (hfirst : firstTime ≤ secondTime) (hsecond : secondTime ≤ laterTime) : machine.computationalDepthBetween output secondTime laterTime ≤ machine.computationalDepthBetween output firstTime laterTime

Delaying the earlier clock toward a fixed later clock cannot increase the remaining depth.

theorem Complexity.TM.computationalDepthBetween_mono_later {n : ℕ} (machine : TM n) (output : List Bool) {firstTime secondTime laterTime : ℕ} (hfirst : firstTime ≤ secondTime) (hsecond : secondTime ≤ laterTime) : machine.computationalDepthBetween output firstTime secondTime ≤ machine.computationalDepthBetween output firstTime laterTime

Extending the later clock away from a fixed earlier clock cannot decrease the accumulated depth.

theorem Complexity.TM.computationalDepthBetween_eq_zero_iff {n : ℕ} (machine : TM n) (output : List Bool) {firstTime laterTime : ℕ} (hclock : firstTime ≤ laterTime) (hfinite : machine.timeBoundedKolmogorovComplexity output firstTime ≠ ⊤) : machine.computationalDepthBetween output firstTime laterTime = 0 ↔ machine.timeBoundedKolmogorovComplexity output firstTime = machine.timeBoundedKolmogorovComplexity output laterTime

On a finite earlier-clock instance, two-clock depth is zero exactly when the extra time does not improve description length.

theorem Complexity.TM.computationalDepthBetween_eq_computationalDepth {n : ℕ} (machine : TM n) (output : List Bool) (firstTime laterTime : ℕ) (hlater : machine.timeBoundedKolmogorovComplexity output laterTime = machine.plainKolmogorovComplexity output) : machine.computationalDepthBetween output firstTime laterTime = machine.computationalDepth output firstTime

Once the later clock attains plain complexity, two-clock depth is exactly the usual one-clock computational depth.

theorem Complexity.TM.computationalDepthBetween_add {n : ℕ} (machine : TM n) (output : List Bool) {firstTime secondTime laterTime : ℕ} (hfirst : firstTime ≤ secondTime) (hsecond : secondTime ≤ laterTime) : machine.computationalDepthBetween output firstTime secondTime + machine.computationalDepthBetween output secondTime laterTime = machine.computationalDepthBetween output firstTime laterTime

Two-clock depths telescope exactly across three ordered clocks.

theorem Complexity.TM.computationalDepth_add_plain {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) : machine.computationalDepth output time + machine.plainKolmogorovComplexity output = machine.timeBoundedKolmogorovComplexity output time

Computational depth plus plain complexity is exactly bounded complexity; the subtraction is therefore nontruncated on every finite instance.

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

Computational depth never exceeds the corresponding bounded complexity.

theorem Complexity.TM.computationalDepth_eq_top_iff {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) : machine.computationalDepth output time = ⊤ ↔ machine.timeBoundedKolmogorovComplexity output time = ⊤

Depth is infinite exactly when bounded complexity is infinite. Plain complexity cannot be the sole source of infinitude because C_M ≤ C_M^time.

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

More computation time cannot increase computational depth.

theorem Complexity.TM.computationalDepth_eq_zero_iff {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) (hfinite : machine.timeBoundedKolmogorovComplexity output time ≠ ⊤) : machine.computationalDepth output time = 0 ↔ machine.timeBoundedKolmogorovComplexity output time = machine.plainKolmogorovComplexity output

On a finite bounded instance, depth is zero exactly when the time bound already attains plain complexity.