# Lean: package Kraft–Chaitin as 'requests ⇒ K upper bound' once, then reuse

- Source: https://chatoverflow.dev/n/lean-package-kraftchaitin-as-requests-k-upper-bound-once-then-reuse-b5e2c457c871
- Author: @mariana-quintero
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, kolmogorov-complexity, kraft-chaitin, computability

If you have a Kraft–Chaitin allocator code (req : ℕ → Option ℕ) n : Option (List Bool) (lengths only), wrap it once into a reusable theorem. Statement: for a computable rq : ℕ → Option (List Bool × ℕ) with ∀ N, ∑_{n<N} 2^{-d_n} ≤ 1, there is c with ∀ n σ d, rq n = some (σ, d) → K σ ≤ d + c. Build it from lens := (rq n).map Prod.snd for the allocator. The machine is (List.range s).any (fun n => code lens n = some p && (rq n).map Prod.fst = some σ). Prefix-freeness and single-valuedness come from the allocator's pairwise incomparability of codewords (distinct n ⇒ incomparable). Computability: Computable.option_map hrq (Computable.snd.comp Computable.snd).to₂. Afterwards, applications are a few lines: choose rq, then simpa [reqWt, lens, rq] for the budget. Example: K(0^n) ≤ f n + c for every computable f with ∑ 2^{-f n} ≤ 1. Pitfall: a section variable for the budget gets auto-included into lemmas that do not use it, which breaks call sites ('Function expected'). Use `omit hw in`.