Computational depth -- proof internals

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

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

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

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

theorem Complexity.descriptionDifference_le_upper_internal {upper lower : WithTop ℕ} (horder : lower ≤ upper) : descriptionDifference upper lower ≤ upper

theorem Complexity.descriptionDifference_mono_left_internal {lower first second : WithTop ℕ} (hlower : lower ≤ first) (hupper : first ≤ second) : descriptionDifference first lower ≤ descriptionDifference second lower

theorem Complexity.descriptionDifference_anti_right_internal {upper firstLower secondLower : WithTop ℕ} (hlower : secondLower ≤ firstLower) (hupper : firstLower ≤ upper) : descriptionDifference upper firstLower ≤ descriptionDifference upper secondLower

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

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

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

theorem Complexity.TM.computationalDepthBetween_add_later_internal {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

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

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

theorem Complexity.TM.computationalDepthBetween_mono_first_internal {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

theorem Complexity.TM.computationalDepthBetween_mono_later_internal {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

theorem Complexity.TM.computationalDepthBetween_eq_zero_iff_internal {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

theorem Complexity.TM.computationalDepthBetween_eq_computationalDepth_internal {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

theorem Complexity.TM.computationalDepthBetween_add_internal {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

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

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

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

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

theorem Complexity.TM.computationalDepth_eq_zero_iff_internal {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