Book IV · Proposition 14

IV.14

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

Every step, checked

• the circle has positive radiusgiven
• the centre is equally distant from every vertexby I.6
• so one circle passes through all fiveby Def.15

What it needs, and what needs it

Needs: I.6 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 (×11)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×15)continuity

The proposition as code

@proposition(
    "IV.14",
    CONSTRUCTION,
    sample=samples.segment,
)
def prop_IV_14(o: Point, a: Point) -> Out:
    """Circumscribe a circle about the regular pentagon of IV.11."""
    hypothesis("the circle has positive radius", o != a)
    vertices = prop_IV_11(o, a).pentagon
    outline(*vertices)
    for vertex in vertices:
        line(o, vertex)
    around = circle(o, vertices[0], "the circumscribed circle")

    because(prop_I_6, o, vertices[0], vertices[1])

    claim("the centre is equally distant from every vertex", "I.6",
          all(eq_len(o, vertex, o, vertices[0]) for vertex in vertices))
    claim("so one circle passes through all five", "Def.15",
          all(on_circle(vertex, around) for vertex in vertices))
    return Out(centre=o, circle=around)