Vaughan wrote in part:
[A "Euclidean space"] has predicates recognizing those line segments of unit length, and those lines passing through the origin, neither of which I remember from Euclid, [...].
Euclid does however talk about right triangles and line segments of equal length (and equal angles but that follows from the other two).
You seem to have answered your main question, but here are two side points: I have seen a definition of "Euclidean space" better than the above (as a real inner product space): a real affine space with a compatible metric and the parallelogram identity. This is equivalent to a torsor of a real inner product space, or to a real affine space modulo length-preserving transformations. I agree that your definition is correct and this is wrong, since Euclid had only relative lengths, not absolute length. But it's worth knowing that the term "Euclidean space" has varied meanings. I can try to track down the reference if you wish. I also think that it's enlightening to look at Tarski's axioms for geometry. These specify a set of points equipped with a ternary and a quaternary relation (betweenness: A lies on the line segment BC; and AB is congruent to CD). Most of the axioms are independent of dimension, and the betweenness- and congruence-preserving bijections are precisely the affine similarities, as you want. (Indeed, preserving betweenness makes it affine; preserving congruence makes it a similarity.) But one final axiom sets the dimension; this states (in effect) that there exist n + 1 points, affinely independent and affinely spanning the space. If you label the first n points (1,0,0,...) through (...,0,0,1) and the last point the origin, then every point has a unique label, and the space becomes \R^n. Thus the difference between the bad "Euclidean space" as \R^n (down to having a specific basis, with no nontrivial automorphisms) and the good Euclid's space as you want to define it is precisely whether the isomorphisms also fix these n + 1 points. (Allowing the isomorphisms to permute the n non-origin points gives us the common "Euclidean space" as a real inner product space; allowing them to permute all of the n + 1 points gives us "Euclidean space" as a torsor of a real inner product space, as in the first section of this post.) --Toby