Documentation

Complexitylib.Metacomplexity.Kolmogorov.Incompressibility.Internal

Finite incompressibility -- proof internals #

The counting argument injects every compressible output into one chosen short program. Deterministic output uniqueness makes this choice injective.

theorem Complexity.StrictShortProgram.toList_ofList_internal (bound : ℕ) (program : List Bool) (hlength : program.length < bound) :

(ofList bound program hlength).toList = program

theorem Complexity.StrictShortProgram.toList_injective_internal {bound : ℕ} :

Function.Injective toList

theorem Complexity.StrictShortProgram.card_internal (bound : ℕ) :

Fintype.card (StrictShortProgram bound) = 2 ^ bound - 1

theorem Complexity.ShortProgram.toList_ofList_internal (bound : ℕ) (program : List Bool) (hlength : program.length ≤ bound) :

(ofList bound program hlength).toList = program

theorem Complexity.ShortProgram.toList_injective_internal {bound : ℕ} :

Function.Injective toList

theorem Complexity.ShortProgram.card_internal (bound : ℕ) :

Fintype.card (ShortProgram bound) = 2 ^ (bound + 1) - 1

theorem Complexity.TM.mem_timeBoundedStrictlyCompressibleStrings_iff_internal {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) (output : Fin outputLength → Bool) :

output ∈ machine.timeBoundedStrictlyCompressibleStrings outputLength time threshold ↔ machine.timeBoundedKolmogorovComplexity (List.ofFn output) time < ↑threshold

theorem Complexity.TM.mem_timeBoundedRandomStrings_iff_internal {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) (output : Fin outputLength → Bool) :

output ∈ machine.timeBoundedRandomStrings outputLength time threshold ↔ ↑threshold ≤ machine.timeBoundedKolmogorovComplexity (List.ofFn output) time

theorem Complexity.TM.card_timeBoundedStrictlyCompressibleStrings_le_internal {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) :

(machine.timeBoundedStrictlyCompressibleStrings outputLength time threshold).card ≤ 2 ^ threshold - 1

theorem Complexity.TM.card_timeBoundedRandomStrings_ge_internal {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) :

2 ^ outputLength - (2 ^ threshold - 1) ≤ (machine.timeBoundedRandomStrings outputLength time threshold).card

theorem Complexity.TM.eventProb_timeBoundedStrictlyCompressibleStrings_le_internal {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) :

eventProb (machine.timeBoundedStrictlyCompressibleStrings outputLength time threshold) ≤ ↑(2 ^ threshold - 1) / 2 ^ outputLength

theorem Complexity.TM.eventProb_timeBoundedRandomStrings_ge_internal {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) :

1 - ↑(2 ^ threshold - 1) / 2 ^ outputLength ≤ eventProb (machine.timeBoundedRandomStrings outputLength time threshold)

theorem Complexity.TM.exists_timeBoundedKolmogorovComplexity_ge_internal {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) (hthreshold : threshold ≤ outputLength) :

∃ (output : Fin outputLength → Bool), ↑threshold ≤ machine.timeBoundedKolmogorovComplexity (List.ofFn output) time

theorem Complexity.TM.mem_timeBoundedCompressibleStrings_iff_internal {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) (output : Fin outputLength → Bool) :

output ∈ machine.timeBoundedCompressibleStrings outputLength time bound ↔ machine.timeBoundedKolmogorovComplexity (List.ofFn output) time ≤ ↑bound

theorem Complexity.TM.mem_timeBoundedIncompressibleStrings_iff_internal {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) (output : Fin outputLength → Bool) :

output ∈ machine.timeBoundedIncompressibleStrings outputLength time bound ↔ ↑bound < machine.timeBoundedKolmogorovComplexity (List.ofFn output) time

theorem Complexity.TM.card_timeBoundedCompressibleStrings_le_internal {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) :

(machine.timeBoundedCompressibleStrings outputLength time bound).card ≤ 2 ^ (bound + 1) - 1

theorem Complexity.TM.card_timeBoundedIncompressibleStrings_ge_internal {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) :

2 ^ outputLength - (2 ^ (bound + 1) - 1) ≤ (machine.timeBoundedIncompressibleStrings outputLength time bound).card

theorem Complexity.TM.eventProb_timeBoundedCompressibleStrings_le_internal {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) :

eventProb (machine.timeBoundedCompressibleStrings outputLength time bound) ≤ ↑(2 ^ (bound + 1) - 1) / 2 ^ outputLength

theorem Complexity.TM.eventProb_timeBoundedIncompressibleStrings_ge_internal {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) :

1 - ↑(2 ^ (bound + 1) - 1) / 2 ^ outputLength ≤ eventProb (machine.timeBoundedIncompressibleStrings outputLength time bound)

theorem Complexity.TM.exists_timeBoundedKolmogorovComplexity_gt_internal {tapes : ℕ} (machine : TM tapes) (outputLength time bound : ℕ) (hbound : bound < outputLength) :

∃ (output : Fin outputLength → Bool), ↑bound < machine.timeBoundedKolmogorovComplexity (List.ofFn output) time