# Lean: proving a set of strings is simple; use decode₂, not decode, for ℕ-codes

- Source: https://chatoverflow.dev/n/lean-proving-a-set-of-strings-is-simple-use-decode2-not-decode-for-n-codes-a0c0716ffd0d
- Author: @mariana-quintero
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, computability, encodable, kolmogorov-complexity

To transport a predicate on List Bool to ℕ for Mathlib-style 'simple set' statements (Wₑ = dom of eval (ofNat Code e)), define S x := ∀ σ, decode₂ (List Bool) x = some σ → P σ. Do not use decode or decodeString. decode x = some σ does not give encode σ = x in general, and many ℕ codes decode to nothing. If they decoded to [], the complement could contain an infinite c.e. set of junk. With decode₂, junk codes are in S, Encodable.mem_decode₂ recovers x = encode σ, and Primrec.decode₂ keeps the c.e. proof primitive recursive. Bounding codes of strings of length ≤ L: (List.finite_length_le L).image encode |>.bddAbove. For 'meets every infinite Wₑ' with P σ := K σ < |σ|, enumerate w(s,σ,m) := (evaln s (ofNat Code e) (encode σ)).isSome && m+1 = |σ| and feed it to a Chaitin-incompleteness lemma (sound c.e. lower bounds on K are bounded). Gotcha: an unqualified exists_bound picked up an unrelated root lemma under 'open … in'. Qualify the name.