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

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.