Book III · Proposition 25

III.25

Given a segment of a circle, to describe the complete circle of which it is a segment.Heath, 1908

Given only an arc, recover the whole circle -- the practical form of III.9, and how a broken rim is completed.

Every step, checked

• the three points lie on one arc and are distinctgiven
• the three given points are equidistant from the centre they determineby Def.15
• the centre found is equidistant from the three given pointsby III.1
• and the circle on it passes through them allby Def.15

What it needs, and what needs it

Needs: III.1

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

Depth: 9 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×4)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×4)continuity

The proposition as code

@proposition(
    "III.25",
    CONSTRUCTION,
    sample=_three_on_a_circle,
    note="Given only an arc, recover the whole circle -- the practical form of "
    "III.9, and how a broken rim is completed.",
)
def prop_III_25(o: Point, a: Point, b: Point, c: Point) -> Out:
    """Only the segment through A, C, B is given; the circle is to be completed."""
    hypothesis("the three points lie on one arc and are distinct",
               eq_len(o, a, o, b) and eq_len(o, a, o, c) and not collinear(a, b, c))
    outline(a, c, b, close=False)

    found = posit(_centre_of(a, c, b), "F")
    completed = circle(found, a, "the completed circle")
    line(found, a)
    line(found, c)

    claim("the three given points are equidistant from the centre they determine",
          "Def.15", eq_len(o, a, o, b) and eq_len(o, a, o, c))
    because(prop_III_1, o, a, c, b)

    claim("the centre found is equidistant from the three given points", "III.1",
          eq_len(found, a, found, b) and eq_len(found, a, found, c))
    claim("and the circle on it passes through them all", "Def.15",
          all(on_circle(point, completed) for point in (a, b, c)))
    return Out(circle=completed, centre=found)