Book IV · Proposition 16

IV.16

In a given circle to inscribe a fifteen-angled figure which shall be both equilateral and equiangular.Heath, 1908

Fifteen because three and five are prime to one another: a third of the circumference less a fifth leaves two fifteenths, and bisecting that gives one.

Every step, checked

• the circle has positive radiusgiven
• the arc between the two vertices is two fifteenths of the circleby IV.11
• and N bisects it, so AN cuts off one fifteenthby III.30
• stepping the chord round the circle reaches fifteen distinct pointsby Post.3
• every vertex lies on the circleby Def.15
• the figure is equilateralby Def.19
• and equiangularby III.27

What it needs, and what needs it

Needs: I.10 III.27 III.30 IV.11

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.19, Def.22, Def.3, Def.4, Post.1, Post.3, Post.5

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×34)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×24)continuity
• the argument reads a 'same_side' fact off the figureorder

The proposition as code

@proposition(
    "IV.16",
    CONSTRUCTION,
    sample=samples.segment,
    note="Fifteen because three and five are prime to one another: a third of the "
    "circumference less a fifth leaves two fifteenths, and bisecting that gives one.",
)
def prop_IV_16(o: Point, a: Point) -> Out:
    """Inscribe a regular fifteen-angled figure, from the hexagon and the pentagon."""
    hypothesis("the circle has positive radius", o != a)
    around = circle(o, a, "the given circle")

    # Euclid's own route. From A, a vertex of the inscribed equilateral triangle
    # stands a third of the way round and a vertex of the pentagon a fifth, so
    # the arc between them is 1/3 - 1/5 = 2/15. Bisecting it gives a fifteenth,
    # and its chord is the side wanted. Nothing here is a formula for the side:
    # it is measured off the figure, as he measures it.
    pentagon = prop_IV_11(o, a).pentagon
    a_fifth = pentagon[1]
    third = circle_with_radius2(a, 3 * len2(o, a), "the chord subtending a third")
    a_third = posit(
        next(point for point in meet(third, around)
             if same_side(point, a_fifth, Line.through(o, a))),
        "T",
    )
    middle = posit(prop_I_10(a_fifth, a_third).midpoint, "M")
    bisected = posit(
        next(point for point in meet(Line.through(o, middle), around)
             if sign((point.x - o.x) * (middle.x - o.x)
                     + (point.y - o.y) * (middle.y - o.y)) > 0),
        "N",
    )
    claim("the arc between the two vertices is two fifteenths of the circle", "IV.11",
          on_circle(a_third, around) and on_circle(a_fifth, around))
    claim("and N bisects it, so AN cuts off one fifteenth", "III.30",
          eq_len(bisected, a_fifth, bisected, a_third))

    side2 = len2(a_fifth, bisected)
    vertices = [a]
    current = a
    for step in range(14):
        stepper = circle_with_radius2(current, side2, f"step {step + 1}")
        onward = [point for point in meet(stepper, around) if point not in vertices]
        if not onward:
            break
        current = posit(onward[0], f"V{step + 2}")
        vertices.append(current)

    claim("stepping the chord round the circle reaches fifteen distinct points", "Post.3",
          len(vertices) == 15)
    outline(*vertices)
    claim("every vertex lies on the circle", "Def.15",
          all(on_circle(vertex, around) for vertex in vertices))
    because(prop_III_30, o, vertices[0], vertices[1])
    because(prop_III_27, o, vertices[0], vertices[1], vertices[2],
            o, vertices[1], vertices[2], vertices[3])

    claim("the figure is equilateral", "Def.19",
          all(eq_len(vertices[i], vertices[(i + 1) % 15], vertices[0], vertices[1])
              for i in range(15)))
    claim("and equiangular", "III.27",
          all(eq_angle(vertices[i - 1], vertices[i], vertices[(i + 1) % 15],
                       vertices[14], vertices[0], vertices[1]) for i in range(15)))
    return Out(polygon=tuple(vertices))