Book IV · Proposition 7

IV.7

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

Every step, checked

• the circle has positive radiusgiven
• each side meets the circle at the end of a radius, and so touches itby III.16
• the four sides are equalby I.34
• and every angle is rightby I.34

What it needs, and what needs it

Needs: 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

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "IV.7",
    CONSTRUCTION,
    sample=samples.segment,
)
def prop_IV_7(o: Point, a: Point) -> Out:
    """Circumscribe a square about the circle, on the tangents at the ends of
    two diameters at right angles."""
    hypothesis("the circle has positive radius", o != a)
    around = circle(o, a, "the given circle")

    reach = (a.x - o.x, a.y - o.y)
    across = _across(o, a)
    corners = []
    for index, (sx, sy) in enumerate(((1, 1), (-1, 1), (-1, -1), (1, -1))):
        corners.append(posit(
            Point(o.x + sx * reach[0] + sy * across[0], o.y + sx * reach[1] + sy * across[1]),
            "EFGH"[index],
        ))
    outline(*corners)

    touching = [
        posit(Point(o.x + reach[0], o.y + reach[1]), "A"),
        posit(Point(o.x + across[0], o.y + across[1]), "B"),
        posit(Point(o.x - reach[0], o.y - reach[1]), "C"),
        posit(Point(o.x - across[0], o.y - across[1]), "D"),
    ]
    for point in touching:
        because(prop_III_16, o, point)
    because(prop_I_34, corners[0], corners[1], corners[2], corners[3])

    claim("each side meets the circle at the end of a radius, and so touches it", "III.16",
          all(on_circle(point, around) for point in touching)
          and all(right_angle(o, touching[i], corners[i]) for i in range(4)))
    claim("the four sides are equal", "I.34",
          eq_len(corners[0], corners[1], corners[1], corners[2])
          and eq_len(corners[1], corners[2], corners[2], corners[3]))
    claim("and every angle is right", "I.34",
          all(right_angle(corners[i - 1], corners[i], corners[(i + 1) % 4]) for i in range(4)))
    return Out(square=tuple(corners))