There are two things here: The proof and how you would represent that in a program that you actually can run.

From the math side, I am confident that the construction and proof can be extended to the real numbers and that can be formalized in lean with minimal changes in the existing proof. (Mathematically speaking, we can replace the rationals with any ordered field and the proof should run through.)

I chose to model the problem with rational numbers because the intersections of polygons with rational coordinates have rational coordinates and rational numbers can easily be represented in the computer.

To have a computable implementation with real numbers, you have to make some choice about which part of the real numbers you want to be able to represent in the computer. For example if sqrt(2) and sqrt(3) is important to you, I think you can have a program that can represent them if they occur in any input coordinates and can represent any resulting coordinates exactly symbolically besides the rational numbers (I think this requires minimal changes in the code, the required lean machinery to work with such numbers can be separated from the geometrical code), but a program can’t be able to represent all real numbers exactly since there are too many of them.

Another interesting direction to take this would be to allow spline segments instead of line segments, since intersections of splines with rational coordinates can have non rational coordinates, but I think can still be represented exactly in the computer. This would require a bigger change and would be interesting geometrically.