I can not agree with the claim that Bitcoin's Script Interpreter is 2PDA as it is defined in Hopcroft et al.
Definition of the 2PDA as given by Hopcroft relies on the notion of looping with the number of loop iterations not known or fixed in advance.
For example: p. 351 (2nd ed), proof of the theorem 8.13 that you referenced, items 5 and 6 state:
5. [Our two-stack machine S] simulates a move of [one-tape Turing machine] M as follows: ....
6. S accepts if the new state of M is accepting. Otherwise, S simulates another move of M in the same way.
Bitcoin script is only capable of doing the "Otherwise, S simulates another move of M in the same way." part a limited, predetermined number of times.
The book introduces the notion of language accepted by PDA and TM in exactly the same way. See, for example, sections 6.2.1 "Acceptance by final state" and 6.2.2 "Acceptance by Empty Stack" that formalize the notion of language accepted by the PDA. Both of them feature "many transition steps" notation, without specifying the upper bound on the number of steps.
If the upper bound is fixed, any language accepted by such PDA could be trivially extended to not be accepted by iteration-limited PDA, but still be accepted by the PDA without iteration limit.
So Bitcoin's Script Interpreter is NOT an implementation of 2-PDA, and Minsky's Theorem is not applicable.