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

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.