Book III · Proposition 29

III.29

In equal circles equal circumferences are subtended by equal straight lines.Heath, 1908

Every step, checked

• the points lie on the circlegiven
• A and B are distinctgiven
• the arcs are arcs of the circles namedby Def.15
• equal arcs are cut off by equal angles at the centresby III.27
• so the chords subtending them are equalby I.4

What it needs, and what needs it

Needs: I.4 III.27

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

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

What it takes on trust

• the argument reads a 'same_side' fact off the figure (×10)order
• the proof evaluates a different number of facts on different configurations (seen: [10, 14, 18]), so it is following more than one route through the diagramcase
• the 'same_side' fact (occurrence 1) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 2) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 5) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 6) is true in some configurations and false in otherscase

The proposition as code

@proposition(
    "III.29",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 3)
    + (samples.isometry(rng),),
)
def prop_III_29(o: Point, a: Point, b: Point, c: Point, move) -> Out:
    """In equal circles, equal arcs are subtended by equal chords."""
    hypothesis("the points lie on the circle",
               eq_len(o, a, o, b) and eq_len(o, a, o, c))
    hypothesis("A and B are distinct", a != b)
    first = circle(o, a, "the first circle")
    p, d, e = posit(move(o), "P"), posit(move(a), "D"), posit(move(b), "E")
    second = circle(p, d, "the second, equal to it")
    line(a, b, "the chord AB")
    line(d, e, "the chord DE")

    claim("the arcs are arcs of the circles named", "Def.15",
          on_circle(a, first) and on_circle(b, first)
          and on_circle(d, second) and on_circle(e, second))
    because(prop_I_4, o, a, b, p, d, e)
    # III.27 speaks of the angles at the circumferences, so each wants a point
    # of its own greater arc to stand at.
    _here = _standing_on_the_major_arc(o, a, b)
    _there = _standing_on_the_major_arc(p, d, e)
    if _here is not None and _there is not None and angle_at(a, o, b) < STRAIGHT:
        because(prop_III_27, o, a, b, _here, p, d, e, _there)

    claim("equal arcs are cut off by equal angles at the centres", "III.27",
          eq_angle(a, o, b, d, p, e))
    claim("so the chords subtending them are equal", "I.4", eq_len(a, b, d, e))
    return Out()