Book XII · Proposition 16

XII.16

Given two circles about the same centre, to inscribe in the greater circle an equilateral polygon with an even number of sides which does not touch the lesser circle.Heath, 1908

Every step, checked

• the two circles are about one centre, and one is the greatergiven
• the lesser circle has a positive radiusgiven
• the two radii describe the plane the circles are ingiven
• the polygon has an even number of sidesby XII.16
• it is equilateral, and inscribed in the greater circleby IV.6
• and no side of it touches the lesser circleby XII.16

What it needs, and what needs it

Needs: IV.6

Used by: XII.17

Rests on: C.N.1, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.17, Def.4, Post.5

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

What it takes on trust

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

The proposition as code

@proposition("XII.16", CONSTRUCTION, sample=samples3.two_radii)
def prop_XII_16(o: Point3, a: Point3, b: Point3) -> Out:
    """In the greater of two circles about one centre, inscribe an equilateral
    polygon with an even number of sides that does not touch the lesser."""
    hypothesis("the two circles are about one centre, and one is the greater",
               sign(len2(o, a) - len2(o, b)) > 0)
    hypothesis("the lesser circle has a positive radius", o != b)
    hypothesis("the two radii describe the plane the circles are in",
               not collinear3(o, a, b))
    greater, lesser = length3(o, a), length3(o, b)
    normal = _axis_of((o, a, b))
    line3(o, a, "the radius of the greater circle")
    line3(o, b, "the radius of the lesser")

    # Bisecting again and again carries the side of the figure past the lesser
    # circle: the perpendicular from the centre to a side is the radius times
    # the cosine of half the angle, and that rises to the radius.
    stage = 2
    while stage < 12 and sign(greater * turn(stage + 1)[0] - lesser) <= 0:
        stage += 1
    corners = _ring(regular_polygon(o, greater, normal, stage),
                    "the polygon inscribed")

    apothem = greater * turn(stage + 1)[0]
    claim("the polygon has an even number of sides", "XII.16",
          len(corners) % 2 == 0 and len(corners) >= 4)
    claim("it is equilateral, and inscribed in the greater circle", "IV.6",
          len({len2(corners[i], corners[(i + 1) % len(corners)])
               for i in range(len(corners))}) == 1
          and all(len2(o, corner) == len2(o, a) for corner in corners))
    claim("and no side of it touches the lesser circle", "XII.16",
          sign(apothem - lesser) > 0)
    return Out(polygon=corners, stage=stage)