How hard would it be to extend this proof to real coordinates? Is that ‘just’ a matter of formalizing some known, tedious math, or would it require new work?
For example, if one allows one coordinate of one corner to be non rational, I think the set of potential output coordinates used would be a subset of the reals (depending on the value of that coordinate), and to my (possibly very bad) intuition, formalizing that subset doesn’t feel like a hard problem.
Allowing two of such real points would make things more tedious, potentially way more tedious, but again, doesn’t feel like it would be impossible to handle.
For example, if one allows one coordinate of one corner to be non rational, I think the set of potential output coordinates used would be a subset of the reals (depending on the value of that coordinate), and to my (possibly very bad) intuition, formalizing that subset doesn’t feel like a hard problem.
Allowing two of such real points would make things more tedious, potentially way more tedious, but again, doesn’t feel like it would be impossible to handle.