Finite incompressibility

At most 2^(k+1)-1 fixed-length strings can have deterministic machine-relative time-bounded Kolmogorov complexity at most k. Consequently, at least 2^n - (2^(k+1)-1) of the n-bit strings exceed k, and one such string exists whenever k < n. In the strict convention used by MINKT, fewer than 2^r strings have complexity below r, so at least 2^n - (2^r - 1) strings are r-random with complexity at least r.

@[simp]

theorem Complexity.StrictShortProgram.toList_ofList (bound : ℕ) (program : List Bool) (hlength : program.length < bound) : (ofList bound program hlength).toList = program

Packaging a strictly bounded list and forgetting the certificate recovers the original list.

theorem Complexity.StrictShortProgram.toList_injective {bound : ℕ} : Function.Injective toList

The variable-length contents uniquely determine a strictly short program.

theorem Complexity.StrictShortProgram.card (bound : ℕ) : Fintype.card (StrictShortProgram bound) = 2 ^ bound - 1

There are exactly 2^r - 1 binary programs of length strictly below r.

@[simp]

theorem Complexity.ShortProgram.toList_ofList (bound : ℕ) (program : List Bool) (hlength : program.length ≤ bound) : (ofList bound program hlength).toList = program

Packaging a bounded list as a short program and forgetting the certificate recovers the original list.

theorem Complexity.ShortProgram.toList_injective {bound : ℕ} : Function.Injective toList

The variable-length contents uniquely determine a short program.

theorem Complexity.ShortProgram.card (bound : ℕ) : Fintype.card (ShortProgram bound) = 2 ^ (bound + 1) - 1

There are exactly 2^(k+1)-1 binary programs of length at most k.

theorem Complexity.TM.mem_timeBoundedStrictlyCompressibleStrings_iff {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) (output : Fin outputLength → Bool) : output ∈ machine.timeBoundedStrictlyCompressibleStrings outputLength time threshold ↔ machine.timeBoundedKolmogorovComplexity (List.ofFn output) time < ↑threshold

Membership in the strict compressible-string set is exactly the MINKT inequality C_U^t(x) < r.

theorem Complexity.TM.mem_timeBoundedRandomStrings_iff {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) (output : Fin outputLength → Bool) : output ∈ machine.timeBoundedRandomStrings outputLength time threshold ↔ ↑threshold ≤ machine.timeBoundedKolmogorovComplexity (List.ofFn output) time

Membership in the complementary random-string set means complexity at least the strict MINKT threshold.

theorem Complexity.TM.card_timeBoundedStrictlyCompressibleStrings_le {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : (machine.timeBoundedStrictlyCompressibleStrings outputLength time threshold).card ≤ 2 ^ threshold - 1

Fewer than 2^r fixed-length strings have time-bounded complexity below the strict threshold r.

theorem Complexity.TM.card_timeBoundedRandomStrings_ge {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : 2 ^ outputLength - (2 ^ threshold - 1) ≤ (machine.timeBoundedRandomStrings outputLength time threshold).card

At least 2^n - (2^r - 1) length-n strings are r-random within the given clock.

theorem Complexity.TM.eventProb_timeBoundedStrictlyCompressibleStrings_le {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : eventProb (machine.timeBoundedStrictlyCompressibleStrings outputLength time threshold) ≤ ↑(2 ^ threshold - 1) / 2 ^ outputLength

Under uniform length-n strings, strict-MINKT probability is at most (2^r - 1) / 2^n.

theorem Complexity.TM.eventProb_timeBoundedRandomStrings_ge {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : 1 - ↑(2 ^ threshold - 1) / 2 ^ outputLength ≤ eventProb (machine.timeBoundedRandomStrings outputLength time threshold)

Uniform fixed-length strings have the complementary quantitative density of r-random strings.

theorem Complexity.TM.exists_timeBoundedKolmogorovComplexity_ge {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) (hthreshold : threshold ≤ outputLength) : ∃ (output : Fin outputLength → Bool), ↑threshold ≤ machine.timeBoundedKolmogorovComplexity (List.ofFn output) time

Whenever r ≤ n, some n-bit string is r-random within every fixed clock.

theorem Complexity.TM.mem_timeBoundedCompressibleStrings_iff {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) (output : Fin outputLength → Bool) : output ∈ machine.timeBoundedCompressibleStrings outputLength time bound ↔ machine.timeBoundedKolmogorovComplexity (List.ofFn output) time ≤ ↑bound

Membership in the compressible-string set is exactly the bounded Kolmogorov-complexity inequality.

theorem Complexity.TM.mem_timeBoundedIncompressibleStrings_iff {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) (output : Fin outputLength → Bool) : output ∈ machine.timeBoundedIncompressibleStrings outputLength time bound ↔ ↑bound < machine.timeBoundedKolmogorovComplexity (List.ofFn output) time

Membership in the incompressible-string set is exactly strict complexity above the bound.

theorem Complexity.TM.card_timeBoundedCompressibleStrings_le {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) : (machine.timeBoundedCompressibleStrings outputLength time bound).card ≤ 2 ^ (bound + 1) - 1

No deterministic machine has more low-complexity outputs than short programs. The bound is independent of the output length and clock.

theorem Complexity.TM.card_timeBoundedIncompressibleStrings_ge {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) : 2 ^ outputLength - (2 ^ (bound + 1) - 1) ≤ (machine.timeBoundedIncompressibleStrings outputLength time bound).card

Quantitative finite incompressibility: all but at most 2^(k+1)-1 of the n-bit strings have time-bounded complexity greater than k.

theorem Complexity.TM.eventProb_timeBoundedCompressibleStrings_le {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) : eventProb (machine.timeBoundedCompressibleStrings outputLength time bound) ≤ ↑(2 ^ (bound + 1) - 1) / 2 ^ outputLength

Under the uniform distribution on n-bit strings, the probability of time-t complexity at most k is at most (2^(k+1)-1) / 2^n.

theorem Complexity.TM.eventProb_timeBoundedIncompressibleStrings_ge {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) : 1 - ↑(2 ^ (bound + 1) - 1) / 2 ^ outputLength ≤ eventProb (machine.timeBoundedIncompressibleStrings outputLength time bound)

Uniform fixed-length strings are quantitatively dense above every time-bounded complexity threshold.

theorem Complexity.TM.exists_timeBoundedKolmogorovComplexity_gt {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) (hbound : bound < outputLength) : ∃ (output : Fin outputLength → Bool), ↑bound < machine.timeBoundedKolmogorovComplexity (List.ofFn output) time

For every clock and every k < n, some n-bit string has time-bounded complexity strictly greater than k.