Book VI · Proposition 18
On a given straight line to describe a rectilineal figure similar and similarly situated to a given rectilineal figure.Heath, 1908
Needs: nothing earlier.
Rests on: Post.1, VI.Def.1
Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@proposition(
"VI.18",
CONSTRUCTION,
sample=lambda rng: samples.quadrilateral(rng) + samples.segment(rng),
)
def prop_VI_18(a: Point, b: Point, c: Point, d: Point, p: Point, q: Point) -> Out:
"""On PQ, describe a figure similar to the given quadrilateral ABCD."""
hypothesis("the given figure is genuine",
not collinear(a, b, c) and not collinear(a, c, d), guard=True)
hypothesis("P and Q are distinct", p != q)
outline(a, b, c, d)
line(p, q, "the given line PQ")
# The similarity carrying AB onto PQ, expressed in the frame of AB itself.
ux, uy = b.x - a.x, b.y - a.y
scale = len2(a, b)
vx, vy = q.x - p.x, q.y - p.y
def carried(point: Point) -> Point:
px, py = point.x - a.x, point.y - a.y
along = (px * ux + py * uy) / scale
across = (px * uy - py * ux) / scale
return Point(p.x + along * vx + across * vy, p.y + along * vy - across * vx)
built = [p, q] + [posit(carried(point), name) for point, name in ((c, "R"), (d, "S"))]
outline(*built)
claim("the figure described is similar to the given one", "VI.Def.1",
all(len2(built[i], built[j]) * len2(a, b) == len2((a, b, c, d)[i], (a, b, c, d)[j])
* len2(p, q) for i in range(4) for j in range(i + 1, 4)))
claim("and it stands on the given straight line", "Post.1",
built[0] == p and built[1] == q)
return Out(figure=tuple(built))