I started writing a simple simulation that generates a distribution of miners with differing efficiency. As I was programming the behavior of the miners, I started by assuming miners will act rationally and always try and maximize their profit, and from there I plan on trying to have individual miners behavior differently and exploit the network.

An interesting consequence of them action rationally is that if the expectation value of their profit per hash E is less than the cost per hash, then they're better off powering down their hashing equipment until the transaction pool fills - assuming they can stop the clock on their ASIC and stop the dynamic power consumption of the ASIC.

I think it should be easy to prove that a rational miner will always mine the largest fee per kb transactions. I would think this proof already exists in a general form somewhere. Let S=[s1, s2, s3...] such that s(n) > s(n-1). Let P = S xor s1 so that P = [s2, s3, s4...] and take S-P you get s1, which means S is larger than P by s1.... errrrrrrrr, did I just prove the axiom of an ordered set? Anyway, someone could probably do this better than me, but the intuitive statement is that if you remove highest fee per kb transactions, you always lower the mean fee per transaction.

For proving a Nash equilibrium exists, I had to look this up, and it seems like an interesting problem. While I think I can say I have a conceptual understanding, the proof is probably beyond my expertise in game theory or my ability to generate rigorous proofs (which is like 5 lectures on open-courseware and what I gleam from my wife - she's a math teacher).