A rational point is an element of \(\mathbb {Q}^2\), represented as a function \(\mathrm{Fin}\, 2 \to \mathbb {Q}\).

For \(u, v \in \mathbb {Q}^2\) we define \(u \times v = u_0 v_1 - u_1 v_0\), \(u \cdot v = u_0 v_0 + u_1 v_1\), and \(\lVert v\rVert ^2 = v_0^2 + v_1^2\).

The map \(R : (x, y) \mapsto (-y, x)\) is a \(90^\circ \) counterclockwise rotation, and preserves squared length.

A (closed, resp. open) half-space is specified by a basepoint \(b \in \mathbb {Q}^2\) and a nonzero inward normal \(n \in \mathbb {Q}^2\); a point \(p\) belongs to the half-space iff \(n \cdot (p - b) \ge 0\) (resp. \({\gt} 0\)).

Given distinct points \(p_1, p_2 \in \mathbb {Q}^2\), the half-space strictly (resp. weakly) to the left of the directed segment \(p_1 \to p_2\) uses basepoint \(p_1\) and normal \(R(p_2 - p_1)\).

A line is a basepoint together with a nonzero direction vector. Two nonparallel lines have a unique intersection point, computed by Cramer’s rule.

Given \(d, \tau {\gt} 0\), one may translate the basepoint of a half-space inward along its normal by an amount in \([d, d+\tau ]\), obtaining a new half-space contained in the original. The scaling factor is realised rationally via Lemma 10.

Given \(0 \le \ell {\lt} u\) in \(\mathbb {Q}\), there is an explicit rational \(r {\gt} 0\) with \(\ell \le r^2 \le u\).