Excellent point, but perhaps termination is just a detail. We already know that it's unsolvable. What's the rush? Next you'll be telling me that different poly

Excellent point, but perhaps termination is just a detail. We already know that it's unsolvable. What's the rush? Next you'll be telling me that different polynomials in P matter, like O(n^27) is too slow or at least requires attention to constants and scale. This construction also solves the divide-by-zero problem very elegantly. When we promote Natural Zero to Real, we make sure that it's something like: (1, λ_:Unit. (1/2, λ_:Unit. (1/3, λ...))) This makes division by zero a legal operation (pointwise division of sequences) if we extend our tolerance to sequences without the Cauchy property (and why not? It's just bits).