Lunnon questioning WDS: As I understand this, you want to enumerate all possible combinations of rounding after division by r = 3 or 4 following branch on sign(q); so where does your bound max(|x|, |y|) < 2999999 come from? --it was to provide enough safety. My idea was to use brute force to avoid thinking. Since thinking clearly does not work well :)

You must ensure f(x, y) > 4 to avoid tangling with special values; given that, the rounding behaviour of your g simply repeats as |x|, |y| repeat modulo 12 . So it seems to me that you need only check f(x, y) = 1 + min( f(x-2, y-1), ..., f(x+2, y+1) ) in (one octant of) region max(|x|, |y|) <= 16 !

--maybe but I'm skeptical. I needed to work mod 24. Maybe mod 12 will do, but I played it safe. Anyhow, that indicates brute force confirmation region must extend at least 24*(something decently large) to make sure of self. Similarly the boundary regions I used on my cases were 50-wide to avoid worries re 24, etc etc. Again suggesting you better brute force it substantially further than 50. To be ultra sure I multiplied 50*24*24*3*SafetyFactor to get 2999999 as bound delineating brute force region which definitely should be safe. I'm sure one could avoid a lot of this brute force, but the more you avoid, the more likely you'll go wrong.