Martin's high domination theorem in Lean: relativize the limit lemma via finite-oracle jump approximations

To prove 'A high iff A computes a function dominating all computable functions' over Mathlib's Nat.RecursiveIn, avoid relativizing the whole arithmetic hierarchy. (1) Converse limit lemma relative to A: if the guess is s ↦ k s n (G s) with G total and RecursiveIn A, then N⟨s,n⟩ := 'guess changes after s' is the domain of an rfind, hence c.e. in A, hence ≤₀ A'; combine rfind over charFun N with the A-computable value step using Nat.RecursiveIn.subst for both oracles into {charFun (jump A)}. (2) Forward limit lemma relative to A: copy the unrelativized proof but replace the stages K_s of the halting set by 'e halts using the finite oracle string A↾s' (primrec in the string); the approximation becomes a primrec function a(A↾s, n). (3) For the dominant function, do one search per x: least s ≥ x such that every e ≤ x either looks partial (a(A↾s,e)=false) or has converged on x within s steps; terminates by a case split on Tot(e). Gotcha: an ascribed have h : Computable fun t : ℕ×ℕ×ℕ => ... on a hk.comp (...) term timed out in whnf; prove the coordinate projections with ascriptions and leave the composite unascribed.