Book IV · Proposition 12

IV.12

About a given circle to circumscribe an equilateral and equiangular pentagon.Heath, 1908

The pentagon of IV.11 turned outside in: its vertices become the points where the circumscribed pentagon touches.

Every step, checked

• the circle has positive radiusgiven
• each side touches the circle at a vertex of the inscribed pentagonby III.16
• the circumscribed pentagon is equilateralby I.47
• and equiangularby I.8

What it needs, and what needs it

Needs: I.8 I.47 III.16 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 (×21)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×39)continuity

The proposition as code

@proposition(
    "IV.12",
    CONSTRUCTION,
    sample=samples.segment,
    note="The pentagon of IV.11 turned outside in: its vertices become the points "
    "where the circumscribed pentagon touches.",
)
def prop_IV_12(o: Point, a: Point) -> Out:
    """Circumscribe a regular pentagon about the circle about O through A."""
    hypothesis("the circle has positive radius", o != a)
    around = circle(o, a, "the given circle")
    touches = prop_IV_11(o, a).pentagon

    tangents = [_tangent_at(o, point) for point in touches]
    corners = [
        posit(meet_one(tangents[index], tangents[(index + 1) % 5]), "GHKLM"[index])
        for index in range(5)
    ]
    outline(*corners)

    for point in touches:
        because(prop_III_16, o, point)
    because(prop_I_47, corners[0], touches[0], o)
    because(prop_I_8, o, touches[0], corners[0], o, touches[1], corners[1])

    claim("each side touches the circle at a vertex of the inscribed pentagon", "III.16",
          all(on_circle(point, around) for point in touches)
          and all(right_angle(o, touches[i], corners[i]) for i in range(5)))
    claim("the circumscribed pentagon is equilateral", "I.47",
          all(eq_len(corners[i], corners[(i + 1) % 5], corners[0], corners[1])
              for i in range(5)))
    claim("and equiangular", "I.8",
          all(eq_angle(corners[i - 1], corners[i], corners[(i + 1) % 5],
                       corners[4], corners[0], corners[1]) for i in range(5)))
    return Out(pentagon=tuple(corners), touching=touches)