Book IV · Proposition 15

IV.15

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

The hexagon is the easy one: its side is the radius exactly, so the compass steps round the circle without being reset.

Every step, checked

• the circle has positive radiusgiven
• stepping the radius round the circle reaches six distinct pointsby Post.3
• every vertex lies on the circleby Def.15
• the hexagon is equilateral, each side equal to the radiusby Def.15
• and equiangularby III.27

What it needs, and what needs it

Needs: III.27

Used by: XIII.9 XIII.10 XIII.12

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

Depth: 14 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 (×5)continuity

The proposition as code

@proposition(
    "IV.15",
    CONSTRUCTION,
    sample=samples.segment,
    note="The hexagon is the easy one: its side is the radius exactly, so the "
    "compass steps round the circle without being reset.",
)
def prop_IV_15(o: Point, a: Point) -> Out:
    """Inscribe a regular hexagon in the circle about O through A."""
    hypothesis("the circle has positive radius", o != a)
    around = circle(o, a, "the given circle")

    side2 = len2(o, a)  # the side of the hexagon is the radius itself
    vertices = [a]
    current = a
    for step in range(5):
        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], "BCDEF"[step])
        vertices.append(current)

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

    claim("the hexagon is equilateral, each side equal to the radius", "Def.15",
          all(eq_len(vertices[i], vertices[(i + 1) % 6], o, a) for i in range(6)))
    claim("and equiangular", "III.27",
          all(eq_angle(vertices[i - 1], vertices[i], vertices[(i + 1) % 6],
                       vertices[5], vertices[0], vertices[1]) for i in range(6)))
    return Out(hexagon=tuple(vertices))