Exactness

6. Exactness (since v0.0)

All coordinates and line coefficients are exact constructible reals (Num; see ADR 0010). A line is a·x + b·y = c with a, b, c ∈ Num.t.

Num.t is a recursive tower of quadratic extensions over ℚ: Rat of Q.t at the base and Ext(a, b, d) = a + b√d for the irrational levels. The ℚ fast-path applies for all values produced by axioms 1–4: their results stay in Rat, so those operations pay no overhead over the previous ℚ representation. The Ext constructor is introduced only by sqrt, which is first needed at axiom 5.

Axioms 1–4 over rational inputs remain closed in ℚ: no square roots arise. At axiom 5 (the angle bisector) the result generally requires square roots — degree-2-or-less extensions of the base field per [hull2020] §3.2. Cube roots do not arise until axiom 6 (the Beloch fold).

Equality, parallelism, and point-in-polygon are therefore exact throughout — no epsilon, no tolerance, no sampling. The only place a float appears is to_float in the serialisation of vertices_coords to FOLD JSON; internal values are never truncated.