@cosmo thank you for posting these results … they are new to me and probably many others!
Anything with a 13.3 in the proof almost surely uses heavy artillery 
Collatz proofs often rely on the exponentially-growing separation between 2^k and 3^x.
There are three that I know about:
-
Baker’s groundbreaking result was that 2^k - 3^x > 3^x \cfrac{a}{b^{k-1}}, for effective constants a and b that he didn’t supply.
-
Rhin’s result was that 2^k - 3^x > \cfrac{0.00220823 3^x}{x^{13.3}}. There’s where any 13.3 probably comes from.
-
Ellison’s result was that 2^k - 3^x > 2.56^x for x > 17.
Ellison’s result is handy for simple jobs, though Rhin’s is better when you need something closer to 3^x. They cross at x=571.
Math kook doesn’t enjoy heavy artillery because he doesn’t understand it. But surely that’s a bad attitude. As von Neumann told a guy who asked a question at a lecture, “Young man, in mathematics you don’t understand things. You just get used to them.”