[ebolyen]

Relatedly, what about integers like 9007199254740995. Is that a legal integer since it rounds to 9007199254740996?

It does seem unclear what it means to exceed precision (given rounding is such an expected part of the way we use these numbers). Magnitude feels easier as at least you definitely run out of bits in the exponent.