Skip to main content

Module constructibility

Module constructibility 

Source
Expand description

Constructibility — compass-and-straightedge feasibility decisions.

A length, angle, or figure is constructible iff it can be produced with compass and straightedge from a unit segment. This is the feasibility gate for the NL→3D-fabrication pipeline: “can this geometric feature be made by this method?” ([[project-nl-to-3d-fabrication-purpose]]). It also settles the three classical impossibilities (doubling the cube, trisecting a general angle, squaring the circle) and decides which regular polygons are constructible (Gauss–Wantzel).

§The decision procedures

  • Degree criterion (Wantzel). A constructible number is algebraic of degree a power of two over ℚ. So constructible_from_min_poly_degree decides every classical case from the minimal-polynomial degree alone: ∛2 (degree 3) → no (doubling the cube); cos(20°) (degree 3) → no (trisecting 60°).
  • Gauss–Wantzel for the regular n-gon: constructible iff n = 2^a · (product of *distinct* Fermat primes). See is_regular_polygon_constructible; the heptadecagon (n = 17) is the showcase.
  • Within the CAS (super::symbolic_algebra::Expr): any well-formed real expression over rationals, the field operations, integer powers and square roots is constructible by construction — square roots are exactly the degree-2 tower. is_constructible_number confirms real-validity and reports the field-extension degree bound; it fails closed on a non-real √(negative) or a division by zero.

Everything here is decidable and verifiable; nothing is fabricated.

Enums§

ConstructibilityVerdict
The verdict for a CAS expression.

Functions§

constructible_from_min_poly_degree
Wantzel’s degree criterion: a number of minimal-polynomial degree degree over ℚ is constructible only if degree is a power of two. (Necessary and, with the quadratic-tower construction, the operative test for the classical problems.)
doubling_the_cube_constructible
The classical impossibilities, decided from the degree criterion (documented facts, not hardcoded opinions): Doubling the cube needs ∛2 — degree 3, not a power of two.
is_central_angle_constructible
The angle 2π/n (a regular-n-gon central angle) is constructible iff the regular n-gon is. So a 60° angle (n = 6) is constructible; 40° (n = 9) is not.
is_constructible_number
Decide constructibility of the number denoted by a CAS expression. Within Expr (rationals + field ops + integer powers + square roots) every well-formed real number is constructible; this confirms real-validity and reports the degree bound, failing closed on √(negative) or ÷0.
is_fermat_prime
A Fermat prime is a prime of the form 2^(2^k) + 1 (3, 5, 17, 257, 65537, …). The constructible odd-prime polygon sides are exactly these.
is_power_of_two
n is a power of two (n ≥ 1).
is_regular_polygon_constructible
Gauss–Wantzel: the regular n-gon is constructible iff n = 2^a · (product of distinct Fermat primes) — i.e. after stripping factors of two, the odd part is a squarefree product of Fermat primes. (n ≥ 3.)
squaring_the_circle_constructible
Squaring the circle needs √π; π is transcendental (no finite minimal polynomial), so it is not algebraic of any finite degree, let alone a power of two.
trisecting_general_angle_constructible
Trisecting a general angle needs a root of 4x³ − 3x − cos θ — degree 3.