Book IV · Proposition 8

IV.8

In a given square to inscribe a circle.Heath, 1908

Every step, checked

• ABCD is a squaregiven
• the centre is equally distant from all four sidesby I.34
• and each of those distances is at right angles to its sideby I.12
• so the circle touches every sideby III.16

What it needs, and what needs it

Needs: I.10 I.12 I.34 III.16

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: 12 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 (×24)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×25)continuity

The proposition as code

@proposition(
    "IV.8",
    CONSTRUCTION,
    sample=samples.square,
)
def prop_IV_8(a: Point, b: Point, c: Point, d: Point) -> Out:
    """Inscribe a circle in 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)

    centre = posit(prop_I_10(a, c).midpoint, "O")
    feet = [posit(prop_I_10(*side).midpoint, "EFGH"[index])
            for index, side in enumerate(((a, b), (b, c), (c, d), (d, a)))]
    inscribed = circle(centre, feet[0], "the inscribed circle")

    because(prop_I_34, a, b, c, d)
    because(prop_I_12, a, b, centre)
    because(prop_III_16, centre, feet[0])

    claim("the centre is equally distant from all four sides", "I.34",
          all(eq_len(centre, foot, centre, feet[0]) for foot in feet))
    claim("and each of those distances is at right angles to its side", "I.12",
          all(right_angle(centre, feet[i], (a, b, c, d)[i]) for i in range(4)))
    claim("so the circle touches every side", "III.16",
          all(on_circle(foot, inscribed) for foot in feet))
    return Out(centre=centre, circle=inscribed)