In that case, the target format problem shows up in the formalisation of the physical system.
A specific formalization of this idea would be that a proof system equipped with an oracle (axiom schema) describing the states of the physical system which allegedly computed these facts, as well as its transition rule, should be able to find proofs for those logical facts in less steps than one without such axioms.
Such proofs will involve first coming up with a mapping (such as interpreting certain electrical junctions as nand gates), proving them valid using the transition rules, then using induction to jump to “the physical state at timestep t is X therefore Alice’s favourite ice cream colour is Y”.
How do you “interpret” certain electrical junctions as nand gates? Either you already have
a proof system equipped with an axiom schema describing the states of the physical system, as well as its transition rule
or this is a not fully formal step. Odds are you already have one (your theory of physics). But then you are measuring proof shortness relative to that system. And you could be using one of countless other formal systems which always make the same predictions, but relative to which different proofs are short and long. To steal someone elses explanation:
Let us imagine a white surface with irregular black spots on it. We then say that whatever kind of picture these make, I can always approximate as closely as I wish to the description of it by covering the surface with a sufficiently fine square mesh, and then saying of every square whether it is black or white. In this way I shall have imposed a unified form on the description of the surface. The form is optional, since I could have achieved the same result by using a net with a triangular or hexagonal mesh. Possibly the use of a triangular mesh would have made the description simpler: that is to say, it might be that we could describe the surface more accurately with a coarse triangular mesh than with a fine square mesh (or conversely), and so on.
And which of these empirically indistinguishable formalisations you use is of course a fact about the map. In your example:
A bit like how it’s more efficient to convince your friend that 637265729567*37265974 = 23748328109134853258 by punching the numbers into a calculator and saying “see?” than by handing over a paper with a complete long multiplication derivation (assuming you are familiar with the calculator and can convince your friend that it calculates correctly).
The assumption (including that it takes in and puts out in arabic numerals, and uses “*” as the multuplication command, and that buttons must be pressed,… and all the other things you need to actually use it) includes that.
I think youve given a good analysis of “simulation”, but it doesnt get around the problem OP presents.
Its also possible to do those calculations during the interpretation/translation. You may have meant that, I cant tell.
Your idea that the computation needs to happen somewhere is good, but in order to make it work you need to specify a “target format” in which the predictions are made. “1″ doesnt really simulate Alice because you cant read the predictions it makes, even when they are technically “there” in a mathematical sense, and the translation into such a format involves what we consider the actual simulation.
This means though, that whether something is a simulation is only on the map, and not in the territory. It depends on a what that “target format” is. For example a description in chinese is in a sense not a real description to me, because I cant process it efficiently. Someone else however, may, and to them it is a real descripton. Similarly one could write a simulation in a programming language we dont know, and if they dont leave us a compiler or docs, we would have a hard time noticing. So whether something is a simulation can depend on the observer.
If we want to say that simulations are conscious and ethically relevant, this seems like something that needs to be adressed.