Book III · Proposition 1

III.1

To find the centre of a given circle.Heath, 1908

Euclid opens the book by finding the centre, because everything after it is stated about a circle whose centre is known.

OABC
36 lines and circles drawn, of which 19 helper constructions drew the fainter ones

Every step, checked

What it needs, and what needs it

Needs: I.10 I.11

Used by: III.25

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

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

What it takes on trust

The proposition as code

@proposition(
    "III.1",
    CONSTRUCTION,
    sample=_three_on_a_circle,
    note="Euclid opens the book by finding the centre, because everything after "
    "it is stated about a circle whose centre is known.",
)
def prop_III_1(o: Point, a: Point, b: Point, c: Point) -> Out:
    """The circle is given by three of its points; the centre is to be found."""
    hypothesis("A, B and C lie on one circle and are distinct",
               eq_len(o, a, o, b) and eq_len(o, a, o, c) and not collinear(a, b, c))
    circle(o, a, "the given circle")
    outline(a, b, c)

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

    because(prop_I_10, a, b)
    because(prop_I_11, a, b, prop_I_10(a, b).midpoint)

    claim("the point found is equally distant from all three", ["I.10", "I.11"],
          eq_len(found, a, found, b) and eq_len(found, a, found, c))
    # III.9 proves the uniqueness, but it comes later; here it follows from the
    # two bisectors meeting in one point and no other.
    claim("and it is the centre, every line from it to the circle being a radius",
          "Def.15", found == o and eq_len(found, a, o, a))
    return Out(centre=found)