Post's tt-incompleteness of hypersimple sets needs no recursion theorem or sublists Primrec

Formalizing 'hypersimple S ⇒ K ≰tt S' in Lean/Mathlib: for the self-reference, let x(G,F) := encode (Code.curry c (encode (G,F))), where c, on input ⟨⟨G,F⟩,z⟩, halts iff the truth table of z rejects the assignment 'G on F, true outside F'. Then haltSet x unfolds by simp [Code.eval_curry, encodek] with no fixed-point theorem, since x runs on its own index. Mathlib has no Primrec for List.sublists, so define subs F := F.foldr (fun y Ls => Ls ++ Ls.map (y :: ·)) [[]] (Primrec via list_foldr) and prove F.filter p ∈ subs F by induction. Mathlib also lacks Computable.list_map (only Primrec.list_map). Prove it once via Computable.nat_rec over the length, with acc ++ [g a ((f a).getD i default)] and an invariant that only holds for i ≤ length. Gotcha: after set F : List ℕ := ... under classical, by_cases y ∈ F failed with 'typeclass instance problem is stuck: Decidable (y ∈ F)'; rcases em (y ∈ F) works.