Efficiently modeling Turing machines in Peano Arithmetic
I am not sure I understand the question, specially the informal part. If by it you mean essentially how we generally argue for correctness of things, I woke interpret it as day proofs in ZFC or something like that.

In any case we can express provability of a statement in a computably axiomatizable system in PA (and in fact in weaker systems). Now you are asking if this can be expressed as efficiently in PA as in the stronger system. The answer is yes, just express that the Turing machine that search for a string is a ZFC proof of the formula halts. The size of the description of such a machine is polynomial in the size of the ZFC formula.

The answer to the second question is no. Just consider a computable function that grows so fast that PA cannot prove its totality but ZFC van prove its totality.



The key idea really is that the language of ZFC itself is very easy to capture. We can express that string $\pi$ is a ZFC-proof of $\varphi$ in much simpler systems that ZFC (e.g. Cook's $V^0$ which captures computation in $AC^0%).

If we can express that, then we can express anything ZFC can express. That is there is polynomial-time computable function $t$ that maps any well-formed formula in the language of ZFC to a formula in the language of PA such that the formula is provable in ZFC iff there is a string that PA proves it is a ZFC proof of the the translation with: just encode the ZFC proof, PA can verify syntactically that it is a valid ZFC proof, and if there is such a string that PA proves is a ZFC proof of the formula, then it is actually a ZFC proof of the formula.

It is key here that I didn't quantify for the existence of the ZFC proof in the PA translation. The reason is that PA might not be able to prove the existence generally. E.g. let $f$ be computable function whose totality is provable in ZFC but not in PA. Then the formula $\forall x \exists y f(x)=y$ is probable in ZFC but not in PA (with any resonable encoding). The reason is that if we can prove it then we prove the totality.

This is generally related to what is called interpretability and interpretation in logic. Essentially we have L1 and L2 and they have their own semantics, and we ask if everything in L1 can be faithfully expressed in L2. Think of the formulas as capturing the subsets of the standard models of those languages. E.g. for ZFC this would be the standard model $\mathbb{V}$ while for PA this would be standard natural numbers $\mathbb{N}$. Before thinking about expressing things, you need to think about how subsets of these two structure map to each other. What does it mean to map a set in ZFC to a set in PA. We can restrict our interest to subsets of $\omega$ in ZFC. Then the question becomes. We can restrict ourselves to arithmetic subsets of $\omega$. Then these subsets are expressible in PA clearly. For any such set we have a PA formula. 

For size we really need to talk about families of formulas. If the family is uniform, that is it is obtained by sectioning another arithmetic formula, then the size relation is still polynomial: let the formulas in ZFC be $\varphi_n(x) := \varphi(n,x)$. To obtain the translation in PA, translate $\varphi$ and then plugin $n$: $[[\varphi_n(x)]] := [[\varphi(x,y)]]_{y/n}$. The only part that changes is $n$, the rest remain the same.

For provability the story is not about standard models but also non-standard models that satisfy the axioms. Is it the case that every function over natural numbers that is total in every model of ZFC is total in every model of PA? The answer is no.