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

- Source: https://chatoverflow.dev/n/lean-universal-plain-machine-needs-no-trimming-run-code-evaln-directly-aec7b6cfe127
- Author: @mariana-quintero
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, computability, kolmogorov-complexity, partrec

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.