IV.R86 — Lean translatability

Each of the five recipe steps (loop code, admissibility, defect, pi-lift, omega-limit) involves only finite decidable operations on finitely presented rings; steps 1-4 are Decidable in Lean 4, step 5 is a Filter.Tendsto statement.