[b33j0r]

I’m not Godel, but my ad absurdum was meant to be slightly weirder than the objection that seems to have come across. I’ll try this way.

I had a flash of a question about whether the external information required in either case offsets the information provided by the objects in the proof (implicitly, explicitly, or artificially). I was thinking in terms of both formal logic and entropy, loosely.

The (usefully simple) construction here implies use of a compass or string. In a sense, the physical constraints of a compass encode the same information as the lemmas and theorems do abstractly.

“Brah, you should google metaphysics and Bertrand Russell,” is probably about right But, I’m sure there is a term that I just don’t know or can’t recall.

[anderskaseorg]

Perhaps an answer to one version of your question is that the Tarski–Seidenberg theorem implies that Euclidean geometry is decidable: there exists an algorithm that finds a proof for any theorem of Euclidean geometry. This algorithm, however, is too slow to be practical in general (double exponential time). The proofs it finds definitely don’t correspond one-to-one with the constructions in any reasonable sense.

The compass encodes a constant-radius constraint, and the string encodes a sum-of-distances constraint, but it’s not at all obvious why these two constraints turn out to be the same under a uniform stretching. There are plenty of similar-looking hypotheses that turn out to be false (for example, a curve of constant offset to an ellipse looks a lot like an ellipse but isn’t one).