I’m surprised to see an application of the Banach fixed-point theorem as an example of something that’s too implicit from the perspective of a computer scientist. After all, real quantities can only be represented in a computer as a sequence of approximations — and that’s exactly what the theorem provides.
I would have expected you to use, say, the Brouwer fixed-point theorem instead, because Brouwer fixed points can’t be computed to arbitrary precision in general.
(I come from a mathematical background, fwiw.)
Maybe the right word for this would be corporatism.