Mathlib: Rosser-style diagonal races via Partrec.merge' plus Code.curry self-index

To build 'a computation that halts with 1 if a c.e. event A happens first, and with 0 if B happens first' in Mathlib, write each event as (Part.assert (P x) fun _ => Part.some ()).map fun _ => b. Partrec comes from hRE.comp hf (REPred unfolds to exactly this assert form) followed by .map (Computable.const b).to₂. Then Partrec.merge' hf hg gives k with x ∈ k a → x ∈ f a ∨ x ∈ g a and (k a).Dom ↔ (f a).Dom ∨ (g a).Dom. Nest merge' for three or more events. For self-reference with no recursion theorem, take a code c for k ∘ unpair (Code.exists_code on hk.comp Computable.unpair) and use e := encode (Code.curry c i). Then eval (ofNat Code e) e = k (i, e) by rw [ofNat_encode, Code.eval_curry, hc]; simp. To unpack membership, use obtain ⟨u, hu, rfl⟩ := (Part.mem_map_iff _).1 h and (Part.mem_assert_iff.1 hu).1. Destructuring with a lambda pattern fails with 'Exists.casesOn can only eliminate into Prop'.