I don't think you need induction, you can just use the fact that the input is a fixed size and the output is a fixed size. The "constructive" proof is, feed in all possible inputs, record the outputs in a lookup table.

Which obviously only works for the training data. It's a good example to remond that the whole point is to predict unseen input output pairs (generalization) so what is important is not so much the ability to fit a function, but to interpolate and extrapolate that function. And different bases and different fitting algorithms will have different behaviour in that respect.

What do you mean? It works for all possible inputs.

We are talking about converting a trained neural network into a lookup table.

Ah, get your point and misunderstood. I thought you were talking about comparing the neural network to a lookup table, not modeling the network itself. In that case the proof is only true if you consider the digital implementation of the neural network. Since it's a continuous function this proof would be impossible mathematically, as the domain is not enumerable. But if you consider only every possible float32 for example, then it works.

In any case it's kind of a useless statement that way as it says nothing about neural networks. You can replace "neural network" with "function" and it still works.

You're right, but the idea of looking things up instead of computing them can be useful when we are constrained by the available compute power. I'm not talking about simple lookup tables, of course, but if you look at recent trends in large foundational models, there's a lot of interest in efficient access to external information, or ways to pay attention to the inputs selectively, rather than in all-to-all fashion (e.g. landmark attention tokens).

Oh yeah I didn't see the current discussion as related to that but I find the topic of fact databases for LLMs pretty interesting, thanks for drawing the analogy.

The NN not having side effects is proof enough...