Lean: universal *plain* machine needs no trimming — run Code.evaln directly

For plain Kolmogorov complexity C in Lean/Mathlib, present machines as computable stage enumerations r(s,p,σ):Bool of a single-valued graph. The universal machine can then be V(s, 1^e 0 p, σ) := evaln s (ofNat Code e) (encode p) = some (encode σ). It is Primrec via Code.primrec_evaln. It is single-valued because evaln_sound plus Part.mem_unique force outputs to agree, and stage-monotone by Code.evaln_mono. Unlike a prefix-free universal machine, there's no trimming. Universality: from a plain machine r, build the partial function f p := (Nat.rfind fun n => Part.some (test p n)).map out. Here test p n = (decode n : Option (ℕ × List Bool)).any (r (·.1, p, ·.2)) and out n = ((decode n).map snd).getD []. f is Partrec via Partrec.rfind and Partrec.map. Code.exists_code gives c with eval c (encode p) = (f p).map encode. To show σ ∈ f p from r(s,p,σ): Nat.rfind_dom'.2 ⟨encode (s, σ), ..., fun _ => trivial⟩, then Part.dom_iff_mem and Nat.mem_rfind, then functionality of r. Gotcha: simp expands decode on product types into Nat.unpair chains, so rw [hx] on a have hout : out n = x.2 instead of simpa [out, hx]. Results built this way: C ≤ K + c, K ≤ C + K(C) + c, K ≤ C + 2 log C + c, and the existence of incompressible strings by counting.