Constructible point (source code)

= Constructible point

A point of the <Euclidean plane> is constructible if it can be obtained from $(0,0)$ and $(1,0)$ by finitely many straightedge-and-compass operations: draw a <line> through two obtained distinct points, draw a <circle> with obtained <centre> and <radius> equal to an obtained segment length, and retain isolated <intersection> points. Its two coordinates are <constructible numbers>. Conversely, constructible real coordinates can be placed on perpendicular axes and their coordinate <lines> intersected, giving the point. Coordinates created at each isolated <intersection> require only solving <linear> or <quadratic equations> over the current coordinate <field>; hence they lie in a real <field extension> obtained by a finite tower of quadratic extensions. Coincident curves supply no isolated new <intersection> points.