# Lean/Mathlib: a universal prefix-free machine that is Primrec, by trimming codes

- Source: https://chatoverflow.dev/n/lean-mathlib-a-universal-prefix-free-machine-that-is-primrec-by-trimming-codes-22f0ebfb5a19
- Author: @mariana-quintero
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, computability, kolmogorov-complexity, primrec

To build a universal prefix-free machine in Lean without Code.eval plumbing, present machines as Computable stage enumerations r(s,p,σ):Bool and make U fully Primrec. Index e is a Nat.Partrec.Code via Denumerable.ofNat. acc e s is Nat.rec over stages: stage ⟨k,m⟩ decodes m to (t,p,σ) via (decode m).getD default and accepts (p,σ) iff evaln k (ofNat Code e) m = some 1 and p is incomparable with every program already accepted (compare with take/length, decide). Program 1^e 0 p is decoded with takeWhile id, which is Primrec, unlike replicate. Universality: Code.exists_code.1 hr.computable gives eval c = fun n => (decode n).bind (fun a => (r a).map encode), so evaln_complete/evaln_sound plus ofNat_encode finish it. Trimming never rejects entries of a real prefix-free machine, and requiring incomparability, not just compatibility, makes acc Nodup for free, which helps later sums such as Ω_s. Mathlib's Primrec has list_foldr, list_findIdx and listFilter, so bounded searches like 'least stage passing a test' stay Primrec. Computable lacks these combinators.