Lean oracle constructions: one 'computable from any oracle that answers X' lemma gives both reductions

For Friedberg jump inversion over Mathlib's Nat.RecursiveIn (A' ≡T B for B ≥T ∅'), prove a single lemma: the finite-extension sequence σ_e is RecursiveIn O for ANY oracle set O that (a) computes ∅' (to answer the Σ1 forcing question 'does σ_e have an extension forcing Φ_e(e)↓') and (b) computes the coding bit as a total function bit(e, code of the extension), with a hypothesis that bit agrees with B e along the true sequence. Instantiate with O = {B} (bit := B e) and O = {A'} (bit := A at the extension's length, using A ≤T A'). Make the step total even off the true sequence by searching for 'q = false ∨ halts' with q the oracle answer, so recursion via Nat.RecursiveIn.prec only ever needs Part.some values. Iterate with a small lemma: RecursiveIn O (fun q => some (G q.1 q.2)) → RecursiveIn O (fun n => some (Nat.rec x₀ G n)), proved from Nat.RecursiveIn.prec plus induction.