Book IV · Proposition 11

IV.11

In a given circle to inscribe an equilateral and equiangular pentagon.Heath, 1908

The high point of Book IV. Its side is the golden section of the radius, so the vertices live in Q(sqrt 5) -- and the kernel keeps them there exactly.

Every step, checked

• the circle has positive radiusgiven
• stepping the chord round the circle reaches five distinct pointsby Post.3
• every vertex lies on the given circleby Def.15
• the pentagon is equilateralby Def.19
• and equiangularby III.27
• the diagonal exceeds the side in extreme and mean ratioby II.11

What it needs, and what needs it

Needs: II.11 III.27

Used by: IV.12 IV.13 IV.14 IV.16 XIII.8 XIII.9 XIII.10 XIII.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: 16 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 (×11)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×14)continuity
• the argument reads a 'same_side' fact off the figure (×10)order

The proposition as code

@proposition(
    "IV.11",
    CONSTRUCTION,
    sample=samples.segment,
    note="The high point of Book IV. Its side is the golden section of the radius, "
    "so the vertices live in Q(sqrt 5) -- and the kernel keeps them there exactly.",
)
def prop_IV_11(o: Point, a: Point) -> Out:
    """Inscribe a regular pentagon in the circle centred at O and through A."""
    hypothesis("the circle has positive radius", o != a)
    around = circle(o, a, "the given circle")

    # The side subtending a fifth of the circumference satisfies
    # s^2 = R^2 (5 - sqrt 5) / 2, which is the golden section of II.11 in disguise.
    side2 = len2(o, a) * (5 - sqrt(5)) / 2
    vertices = [a]
    current = a
    for step in range(4):
        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], "BCDE"[step])
        vertices.append(current)

    claim("stepping the chord round the circle reaches five distinct points", "Post.3",
          len(vertices) == 5)
    for index in range(5):
        line(vertices[index], vertices[(index + 1) % 5])

    claim("every vertex lies on the given circle", "Def.15",
          all(on_circle(vertex, around) for vertex in vertices))
    claim("the pentagon is equilateral", "Def.19",
          all(eq_len(vertices[i], vertices[(i + 1) % 5], vertices[0], vertices[1])
              for i in range(5)))
    # Equal sides cut off equal arcs, and III.27 makes the angles standing on
    # them equal. The circle is compared with itself, which III.27 allows: two
    # equal circles are what it asks for, and no circle is unequal to itself.
    if len(vertices) == 5:
        for index in range(5):
            first, second = vertices[index], vertices[(index + 1) % 5]
            third, fourth = vertices[(index + 1) % 5], vertices[(index + 2) % 5]
            here = _standing_on_the_major_arc(o, first, second)
            there = _standing_on_the_major_arc(o, third, fourth)
            if here is not None and there is not None:
                because(prop_III_27, o, first, second, here, o, third, fourth, there)

    claim("and equiangular", "III.27",
          all(eq_angle(vertices[i - 1], vertices[i], vertices[(i + 1) % 5],
                       vertices[4], vertices[0], vertices[1]) for i in range(5)))
    because(prop_II_11, vertices[0], vertices[2])

    golden = (sqrt(5) - 1) / 2
    claim("the diagonal exceeds the side in extreme and mean ratio", "II.11",
          length(vertices[0], vertices[2]) * golden == length(vertices[0], vertices[1]))
    return Out(pentagon=tuple(vertices))