Lean/Mathlib: Kraft-Chaitin and Levin-Schnorr without a universal machine

To formalize Levin-Schnorr cheaply, present a prefix-free machine as a Computable stage enumeration r(s,p,σ) : Bool of a single-valued graph with prefix-free domain. Then 'σ compressed by c bits' is REPred via REPred.exists_of_computable₂ (pair stage and program), with no Code.evaln plumbing. State randomness as 'for every such machine ∃c ∀n K_M(X↾n) > n-c', which needs no universal machine. Kraft on a finite prefix-free set is the martingale Kraft inequality for the constant martingale 1. For Kraft-Chaitin, keep free strings with pairwise DISTINCT lengths and serve request d from the longest free string of length ≤ d (cut τ0^{d-|τ|}, free τ0^i1). Distinct lengths > d weigh < 2^{-d}, so the allocator never gets stuck. Mathlib has no Primrec for List.erase/replicate: use a foldr-based erase and map-over-range for replicate, proved equal on duplicate-free lists.