Book IV · Proposition 9

IV.9

About a given square to circumscribe a circle.Heath, 1908

Every step, checked

• ABCD is a squaregiven
• the diameters bisect one anotherby I.34
• the centre is equally distant from all four cornersby I.6
• so one circle passes through all fourby Def.15

What it needs, and what needs it

Needs: I.6 I.10 I.34

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

Depth: 11 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 (×8)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×9)continuity

The proposition as code

@proposition(
    "IV.9",
    CONSTRUCTION,
    sample=samples.square,
)
def prop_IV_9(a: Point, b: Point, c: Point, d: Point) -> Out:
    """Circumscribe a circle about the square ABCD."""
    hypothesis("ABCD is a square",
               eq_len(a, b, b, c) and eq_len(b, c, c, d) and eq_len(c, d, d, a)
               and right_angle(d, a, b))
    outline(a, b, c, d)
    line(a, c, "the diameter AC")
    line(b, d, "the diameter BD")

    centre = posit(prop_I_10(a, c).midpoint, "O")
    around = circle(centre, a, "the circumscribed circle")

    because(prop_I_34, a, b, c, d)
    because(prop_I_6, centre, a, b)

    claim("the diameters bisect one another", "I.34",
          centre == prop_I_10(b, d).midpoint)
    claim("the centre is equally distant from all four corners", "I.6",
          all(eq_len(centre, corner, centre, a) for corner in (b, c, d)))
    claim("so one circle passes through all four", "Def.15",
          all(on_circle(corner, around) for corner in (a, b, c, d)))
    return Out(centre=centre, circle=around)