The One Four Problem

One of my favorite books of all time is The Man Who Counted, by Malba Tahan. I first read it in 2011, and it influenced me to become interested in mathematics. The book contains various mathematical puzzles embedded in a wider story. One of the problems is as follows: using only four of the digit 4, mathematical symbols, and no other digits, can you make every integer? For example, 1 is equal to (4+4)/(4+4), or 4 - 4 + (4/4).

Actually, if we interpret "mathematical symbol" as one of the operators (+, -, /, *), then we only have a finite number of expressions that contain exactly four fours, so we definitely can't make every integer! However, by stretching the definition of mathematical symbol, it's possible to do even better than the original problem: we can make every integer with just 1 four! I've written a proof of this fact that you can read here.

I later translated this proof into Coq, with a minor caveat that I'm using the floor of the natural log operation instead of doing log and then floor separately.