Findings

Measured — the Elements leaves the rationals on its first page

Every magnitude these constructions produce is an exact element of a tower of quadratic extensions of the rationals, so it has a degree, and the kernel can state it. Running all 465 propositions gives a map of the work by algebraic depth. The text cannot tell you this; it is a property of what the constructions do.

The equilateral triangle of I.1 already needs √3, and I.2 already needs a second square root standing on the first. Yet Books III and VI — all those circles, all that similarity — never exceed degree 2, and Books VII to IX never leave the rationals at all, which is what arithmetic ought to look like. The deepest point in the whole work is X.115, at degree 32.

euclid measure --depth

Exhaustive — Book X cannot name every constructible number

Book X sorts the irrationals into thirteen named species, and is often described as though that were all of them. A constructible number of degree at most four lies in some Q(sqrt m, sqrt n), where it is a + b·sqrt m + c·sqrt n + d·sqrt(mn). Taking every such number with coefficients up to 2 in size and m < n squarefree up to 11, in order of height, the simplest Euclid has no word for is

1 + sqrt2 + sqrt3  ≈  4.14626437

It is constructible with straightedge and compass, its degree over the rationals is 4, and its minimal polynomial is x^4 - 4*x^3 - 4*x^2 + 16*x - 8 = 0. The classifier's own reason is the whole of the explanation: it resolves into 3 terms, where Book X's definitions treat two. Euclid classifies what comes out of applying areas, which is sums and differences of two terms, so a number needing three falls outside however constructible it is. The enumeration holds 6510 magnitudes; Book X names 1134 of them and has no word for 5376. Height ties are broken by preferring the form written without a subtraction, and the bound is a bound: a constructible of degree 8, or one with a larger radicand, lies outside the set and is not searched.

euclid gap --all

Empirical — II.9 and II.10 are one proposition, written twice

Both say that the squares on the two segments of a divided line are double the square on the half together with the square on the piece between the points of section. II.9 states it for a point taken between the ends; II.10 for a point taken beyond them. Breaking that hypothesis and running anyway, the conclusion holds either way — in every configuration tried (5 of them for II.9).

The identity does not care where the point falls on the line. Euclid needs two propositions because he has no negative length to let one cover both cases; carried out in exact arithmetic the distinction disappears, and the hypothesis separating them does no work.

euclid measure --needless

Empirical — breaking Euclid's hypotheses on purpose

A proposition says nothing about the configurations its hypotheses exclude, so those are normally thrown away, and one question goes unasked: would the conclusion have held anyway? Lifting the exclusion makes it askable. Move one given until a hypothesis breaks, then run without enforcing it.

Across the corpus 868 hypotheses are stated. 868 could be broken cleanly enough to judge (100% coverage — a run that breaks two at once says nothing about either and is discarded). Of those, 276 proved necessary, a claim failing the moment they went, and 44 turned out to be holding the construction together, which is a weaker kind of necessity.

38 survived being broken. Those are candidates, not results, and the likeliest reading of one is that our claims are too weak to notice the difference. That is what happened the first time this ran: seven propositions of Book III were checking things true of any four points, circle or no circle. They were strengthened, and their hypotheses became necessary.

euclid measure --needless

Measured — Euclid uses something his own rules do not give him

His postulates let you draw a circle. None of them says that two circles ever cross. He needs them to cross in I.1, on the very first page, to get the top corner of his triangle — and simply takes it. The gap was not stated properly until the nineteenth century.

Every step that uses an intersection the postulates do not license is counted as it happens: 2573 places across Books I to X. The full ledger →

euclid ledger

Measured — every square root in the corpus is one of three things

Restricting the field a construction may build in and running the corpus again is Hilbert's method: make a model where an axiom fails and see what breaks. Over the rationals no new root is allowed at all. Over the Pythagorean field only roots of sums of two squares are, which is what a straightedge and a way to carry a segment produce — a length may be measured, two circles may not be crossed. Between the two rungs, every root the corpus takes sorts into measuring, crossing, or the proposition's own irrational subject.

The two cases that show what the split is for: I.1 stops in construct.py:_line_circle:163 asking for sqrt(4/75), and no rung short of the full constructibles gives it. I.34, on the opposite sides of a parallelogram, stops in angles.py:between_rays:58 asking for sqrt(32) — and completes over the Pythagorean field, because it only ever measures. It is true in the rational plane, and it appears to fail there only because our encoding builds a root where squared lengths would do.

17 propositions (I.22, I.24, I.25, I.31, I.32, I.38, I.39, I.40, I.43, III.7, III.8, VI.1, VI.10, VI.2, VI.20, VI.24, VI.4) complete over the Pythagorean field while the ledger records them crossing a circle. Their samplers hand them rational triangles, so the circles meet where the configuration already was. Counting those as Pythagorean would be a finding about our test data, so they are kept apart.

The 81 untestable propositions are mostly Book X, whose samplers build irrational magnitudes because that is the subject. A proposition that completes here did so on the rational configurations tried, which is evidence and not a proof of validity in the rational plane.

euclid measure --fields

Measured — four proofs take more than one route through the diagram

A standing worry about old geometry is that a proof may hold only for the figure its author happened to draw. Each proposition is run on many configurations and the runs compared, looking for a step that holds in one figure and fails in another. 11 do: III.2, III.14, III.23, III.24, III.29, III.32, III.33, III.34, VI.9, VI.11, XII.17.

Three of them evaluate a different number of facts depending on where the points fall — III.34 checks between four and nine things about the same theorem — which means the argument is branching on the picture. III.32 is the sharper case: a step asserting two points lie on the same side of a line is true in some configurations and false in others. That is exactly the shape of the gap Pasch's axiom was later written to close.

The other 454 take the same route through every figure they are handed. Configurations have to be built to satisfy a proposition's hypotheses, so one draw in six is now taken from a deliberately awkward range — a large denominator puts a point very near a lattice position without landing on it, which is what makes a triangle nearly flat or a triple nearly collinear. That range found an assumption Euclid leaves unstated in III.14: a chord through the centre is bisected by it, so the perpendicular he drops has no length and there is no line to draw.

The ledger →

euclid ledger

Exhaustive — Euclid's first construction cannot be beaten

For 9 of these problems every shorter figure was enumerated in exact arithmetic and none reached the goal, so fewest possible is a theorem. The two circles of I.1 are the shortest way to an equilateral triangle, and nothing of one move comes close.

Mohr in 1672 and Mascheroni in 1797 proved the compass alone finds anything the pair can, and the search puts a price on it: a midpoint costs six circles, and every five-circle figure was enumerated exactly to prove it cannot be done in five.

That number was seven here until the enumeration reached it. The float search covered depth six and reported nothing, which is exactly the failure the exact pass exists to catch: a point pair merged at a tolerance of 10⁻⁷, or two figures sharing a rounded fingerprint, and a real construction becomes invisible. The six-circle construction it missed replays through the kernel and reaches the midpoint.

Some of Euclid's own constructions are far longer than they need to be, because he builds them out of results already proved, buying certainty with moves.

euclid optimize midpoint --isa compass-only --depth 7