Lean: c.e. in ∅″ ⇒ Σ₃ via use principle + lists of witnesses for 'σ ⊑ ∅″'

To prove 'P c.e. in ∅″ ⇒ P is Σ₃' (concrete ∃y∀z∃w over a computable matrix) without a general arithmetic hierarchy: take the use functional F and its code; P n iff ∃σ, t with the code halting on ⟨σ, n⟩ in t steps and σ ⊑ ∅″. Using a Σ₂ normal form i ∈ ∅″ ↔ ∃y∀z J(i,y,z), put into the outer ∃ a list Y of witnesses for the 1-bits, into the ∀ a pair ⟨y, z⟩, and into the inner ∃ a list Z (decoded with ofNat (List ℕ)) of refutations for the 0-bits: matrix = halts ∧ ∀ i<|σ| (σ_i → J(i, Y_i, z)) ∧ ∀ i<|σ| (¬σ_i → ¬J(i, y, Z_i)). The bounded ∀ i folds into List.any over range. Forward direction builds Y and Z with classical choose inside List.map over range. Pitfall: simp may leave (Nat.unpair (Nat.pair y 0)).1 unreduced inside a hypothesis used with exact; rewrite Nat.unpair_pair explicitly.