Book III · Proposition 30

III.30

To bisect a given circumference.Heath, 1908

Bisecting an arc, which IV.16 needs to reach the fifteen-angled figure.

Every step, checked

• A and B lie on the circle and are distinctgiven
• AB is not a diametergiven
• C lies on the circleby Def.15
• and the two chords to it are equal, so the arc is bisectedby I.4

What it needs, and what needs it

Needs: I.4 I.10

Used by: IV.16 XIII.9 XIII.10

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

Depth: 8 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 (×5)continuity

The proposition as code

@proposition(
    "III.30",
    CONSTRUCTION,
    sample=_two_on_a_circle,
    note="Bisecting an arc, which IV.16 needs to reach the fifteen-angled figure.",
)
def prop_III_30(o: Point, a: Point, b: Point) -> Out:
    hypothesis("A and B lie on the circle and are distinct",
               eq_len(o, a, o, b) and a != b)
    hypothesis("AB is not a diameter", not collinear(a, o, b))
    around = circle(o, a, "the given circle")
    line(a, b, "the chord AB")

    middle = posit(prop_I_10(a, b).midpoint, "D")
    reaching = line(o, middle, "the line from the centre through D")
    halves = [point for point in meet(reaching, around)
              if sign((point.x - o.x) * (middle.x - o.x)
                      + (point.y - o.y) * (middle.y - o.y)) > 0]
    bisection = posit(halves[0], "C")

    because(prop_I_4, middle, a, bisection, middle, b, bisection)

    claim("C lies on the circle", "Def.15", on_circle(bisection, around))
    claim("and the two chords to it are equal, so the arc is bisected", "I.4",
          eq_len(a, bisection, b, bisection))
    return Out(bisection=bisection)