If NP=EXPTIME, does every DTM have a succinct "execution proof"? Let HALTS-IN-N be the canonical $EXPTIME$-complete language {<$M$,$n$> | the deterministic Turing machine (DTM) encoded by $M$ halts in $n$ or fewer steps, with $n$ encoded in binary}.  Since HALTS-IN-N is accepted in $EXPTIME$ by simulating $M$ for $n$ steps (or until it halts, whichever comes first), its complement is also $EXPTIME$-complete just by swapping the "accept" and "reject" states.
Define the execution trace of a DTM to be the string of transitions its finite control goes through in the process of accepting an input.
A language is in $NP$ if each string in the language has a polynomially-sized certificate with which that string's membership in the language can be verified in polynomial time.
Now suppose $NP=EXPTIME$.  Then every instance of HALTS-IN-N has a certificate that $M$ halts in $n$ steps, and this certificate has size polynomial in the size of <$M$,$n$>, which has size logarithmic in the size of $M$'s execution trace (because $n$ is encoded in binary.)
Put another way, the fact that any DTM has halted or not after $n$ steps has two witnesses: its execution trace (size $n$) and its certificate (size logarithmic in $n$).

Question 1: Is the above reasoning valid?

I think the biggest candidate for a hole in it is that I'm assuming |$M$| is essentially a constant.  For a particular $M$ it is, but I don't know if it poses problems when generalizing the statement to every DTM.

Question 2 (soft): If it is valid, how surprising are the consequences?

It sounded quite surprising to me initially, but then I started looking at execution traces of Busy Beaver TM's and realized that there is a lot of redundancy in them; it's not unimaginable to me that a DTM that halts in 47 million steps could have a proof of that fact that is much shorter.
But this part still does seem surprising: in this scenario, you could apparently "run" a DTM not by simulating it step-by-step, but rather by searching for this logarithmically-shorter execution proof.
In fact, what prevents me from finding an execution proof in exponential time even when $M$ represents some problem known to be outside $EXPTIME$?  I can't see it yet, but there must be something; it's inconceivable that $NP$ and $EXPTIME$ could be separated with such a simple argument!

EDIT: As Emil Jeřábek pointed out, I meant polylogarithmic when I wrote logarithmic (apologies for the sloppiness.)  Perhaps I should also have added "(relative to the surprisingness of other known consequences of NP=EXPTIME)" to question 2.
I'll try to give a concrete example for my last paragraph.  Consider a DTM that initially writes an encoding of a primitive recursive function to its tape and which then proceeds to simulate that function, reading it off the tape -- call this machine $M$.  An upper bound (not tight) on the maximum running time of the function should not be difficult to discover by examining its loops -- call this $n$.  Have the DTM halt immediately if the function computes some value, but have it loop $n$ more times before halting if it computes some other value.  (Or use some equivalent trick to tie the result of the function to the number of steps in which the DTM halts.)
The set of such DTMs is outside $PR$ (which is known to be outside $EXPTIME$), but still in $R$, as they always halt.  But such <$M$,$n$> pairs could be given as instances of HALTS-IN-N, and (under the assumption $NP=EXPTIME$) proofs that they halt or not in $n$ steps could be found in time exponential in |<$M$,$n$>|.
Is it just that $n$ is necessarily so enormous that |<$M$,$n$>| is itself enormous, so that time exponential in it is in the territory of the Ackermann function?
 A: Q1: Yes (except that the certificates you get may have size polylogarithmic in $n$, not just logarithmic, and you need to apply the argument to both HALTS-IN-N and its complement, as pointed out by Andreas).
Q2: Well, NP = EXP contradicts all kinds of conjectures from complexity theory: it makes the polynomial hierarchy collapse to NP = coNP, it makes NP = PSPACE, and PSPACE = EXP, all of which are assumed to be false. On the other hand, it also implies P ≠ NP. We cannot rule out NP = EXP with the present state of knowledge (nor the even stronger collapse ZPP = EXP), but the time hierarchy theorem implies that $\mathrm P\ne\mathrm{EXP}$ and $\mathrm{NP}\ne\mathrm{NEXP}\cap\mathrm{coNEXP}$. Existence of succinct certificates also shows up in other similar situations: for example, if EXP has polynomial-size Boolean circuits, then membership in any EXP language has succinct certificates verifiable in randomized polynomial time (that is, EXP = MA).
Vis-à-vis the last but one paragraph of your question, note that an exhaustive deterministic search for a short certificate takes time exponential in the size of the certificate, so you don’t save here anything in terms of deterministic running time.
I don’t follow the last paragraph. EXP = NP implies $\mathrm{DTIME}(2^{t(n)})\subseteq\mathrm{NTIME}\bigl(t(n)^{O(1)}\bigr)$ for every time-constructible function $t(n)$ of at least polynomial growth, if that’s what you mean, but this does not lead to a contradiction.
EDIT: It may be worth mentioning that there is nothing particularly revolting about the idea that the existence of an exponentially long computation can be proved using a polynomial amount of data. In fact, Babai, Fortnow, and Lund have shown that NEXP = MIP, which means that two (computationally unlimited) agents presenting polynomial-size evidence who cannot communicate with each other can reliably convince a randomized polynomial-time verifier that such an exponentially long halting computation (even nondeterministic) exists. (Here, polynomial and exponential is measured in terms of the length of the input, which is logarithmic in the $n$ from the original question.)
EDIT 2: Yes, the running times for primitive recursive functions (or predicates) are enormous. More precisely, a function is primitive recursive if and only if it is computable in time $A(k,n)$ for some constant $k$, where $A$ is the Ackermann function. Plugging an extra exponential or logarithm in this characterization makes no difference. In view of the latter fact, whether NP = EXP or not has not much to do with the argument: we know unconditionally that the version of HALTS-IN-N where $n$ is given in unary is in P.
