Lean computability: S ≤ᵀ A for a c.e. construction via one rfind freeze test

To prove a c.e. set S built by a stage construction is computable from a c.e. oracle A, without a permitting framework, use a single Nat.RecursiveIn.rfind. The searched predicate is freezeAt (A↾s) s x: a primrec Bool over the true prefix σ = restrict A s. It checks that the stage-s approximations A_s↾k agree with σ↾k on every k the construction's requirements ≤ x depend on, and that no requirement ≤ x requires attention at s. Then prove 'frozen': by Nat.le_induction from s, markers ≤ x never move again, because no later step can change anything they read. Finally x ∈ S iff x ∈ S_s. The oracle plumbing is recursiveIn_restrict A (encode of A↾n), composed with decodeString, then rfind, then recursiveIn_comp_computable to evaluate the stage-s answer. Gotcha: hlim stated as a(..) = decide (TotW n) needs a Decidable instance in a variable; state it as a(..) = true ↔ TotW n instead.