Book IV · Proposition 6

IV.6

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

Every step, checked

• the circle has positive radiusgiven
• the two diameters are at right anglesby I.11
• every vertex lies on the circleby Def.15
• the four sides are equalby I.4
• and every angle is right, standing on a diameterby III.31

What it needs, and what needs it

Needs: I.4 I.11 III.31

Used by: XII.16

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

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

The proposition as code

@proposition(
    "IV.6",
    CONSTRUCTION,
    sample=samples.segment,
)
def prop_IV_6(o: Point, a: Point) -> Out:
    """Inscribe a square in the circle about O through A, on two diameters at
    right angles."""
    hypothesis("the circle has positive radius", o != a)
    around = circle(o, a, "the given circle")

    across = _across(o, a)
    c = posit(Point(o.x - (a.x - o.x), o.y - (a.y - o.y)), "C")
    b = posit(Point(o.x + across[0], o.y + across[1]), "B")
    d = posit(Point(o.x - across[0], o.y - across[1]), "D")
    line(a, c, "the diameter AC")
    line(b, d, "the diameter BD, at right angles to it")
    outline(a, b, c, d)

    because(prop_I_11, a, c, o)
    because(prop_I_4, o, a, b, o, b, c)
    because(prop_III_31, o, a, c, b)

    claim("the two diameters are at right angles", "I.11", right_angle(a, o, b))
    claim("every vertex lies on the circle", "Def.15",
          all(on_circle(v, around) for v in (a, b, c, d)))
    claim("the four sides are equal", "I.4",
          eq_len(a, b, b, c) and eq_len(b, c, c, d) and eq_len(c, d, d, a))
    claim("and every angle is right, standing on a diameter", "III.31",
          all(right_angle(*corner) for corner in
              ((a, b, c), (b, c, d), (c, d, a), (d, a, b))))
    return Out(square=(a, b, c, d))