Question: Is the computational cost of verifying the proof significantly less than the computational cost of creating the proof?

Like I haven't run Coq but I assume that in this particular instance, the answer is a rather trivial "yes"? You'd think about, creating this proof is a gigantic research slog and publishable result; verifying it is just looking at the notes you wrote down about what worked (this turing machine doesn't halt and here's the input and here's the repetitive sequence it generates, that turing machine always halts and here's the way we proved it...).

But taken more generally, not for this specific instance, your question is actually a Millenium Prize problem worth a million dollars.

The compiled proof does take a few hours to finish verifying on a typical laptop. But obviously the many experiments and enumerations along the way took much more total processing power.

This is true in general for every mathematical proof in ZFC (and even in more powerful theories). The decision problem "Given a formula F and an integer n, is there a ZFC proof of F of length <= n?" is NP complete, meaning that verifying the proof can be done in polynomial time while deriving the proof can require an exponential amount of time.