Book XII · Proposition 1

XII.1

Similar polygons inscribed in circles are to one another as the squares on the diameters.Heath, 1908

Every step, checked

• the four points are on one circle about the centregiven
• they are not all in one straight linegiven
• the polygons are similar, their sides in one ratioby VI.Def.1
• as the polygon is to the polygon, so is the square on the diameter to the square on the diameterby XII.1

What it needs, and what needs it

Needs: nothing earlier.

Used by: XII.2

Rests on: VI.Def.1

Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition("XII.1", THEOREM, sample=samples3.circle_in_space)
def prop_XII_1(o: Point3, a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Similar polygons inscribed in circles are to one another as the squares
    on the diameters."""
    hypothesis("the four points are on one circle about the centre",
               len2(o, a) == len2(o, b) == len2(o, c) == len2(o, d))
    hypothesis("they are not all in one straight line", not collinear3(a, b, c))
    _ring((a, b, c, d), "the polygon in the first circle")

    # The second circle and the polygon in it are the first carried over in one
    # ratio, which is what makes the figures similar and similarly inscribed.
    ratio = Fraction(5, 3)
    centre = posit3(Point3(o.x + 8, o.y, o.z), "P")
    carried = tuple(posit3(Point3(centre.x + ratio * (point.x - o.x),
                                  centre.y + ratio * (point.y - o.y),
                                  centre.z + ratio * (point.z - o.z)))
                    for point in (a, b, c, d))
    _ring(carried, "the polygon in the second circle")

    here, there = polygon_area((a, b, c, d)), polygon_area(carried)
    across, beyond = 4 * len2(o, a), 4 * len2(centre, carried[0])
    claim("the polygons are similar, their sides in one ratio", "VI.Def.1",
          all(len2(carried[i], carried[j]) == ratio * ratio * len2(one, other)
              for (i, j), (one, other) in
              zip(((0, 1), (1, 2), (2, 3), (3, 0)),
                  ((a, b), (b, c), (c, d), (d, a)))))
    claim("as the polygon is to the polygon, so is the square on the diameter "
          "to the square on the diameter", "XII.1", here * beyond == there * across)
    return Out(areas=(here, there), squares=(across, beyond))