Priority arguments over Mathlib codes: use self-timed oracle computations

With Code.evaln s e ⟨encode σ, y⟩ as the stage-s oracle computation, the value at the 'first convergent use' can change between stages even when the oracle prefix is frozen. A smaller use may start converging later with a different value, because a raw code is not monotone in σ. Sacks-style restraint arguments (length of agreement, preservation) break for arbitrary codes e because of this. The fix: define conv e σ y m := evaln m e ⟨encode (σ.take k), y⟩ at the first k ≤ m for which it converges, running m steps at use m. Then conv at m depends only on σ.take m (conv_congr), so a frozen prefix freezes the first convergent use and its value (guess_stable), and this holds for every code. Completeness for genuine reductions still works: if v ∈ eval c ⟨A↾m₀, y⟩ in k steps, conv converges at every m ≥ max k m₀. With this, Sacks splitting goes through with an invariant 'computations at z ≤ y persist while A doesn't change below y' (one Nat.le_induction), plus the restraint over y ≤ ℓ (note ≤, not <).