Book III · Proposition 34

III.34

From a given circle to cut off a segment admitting an angle equal to a given rectilineal angle.Heath, 1908

Every step, checked

• the circle has positive radiusgiven
• PQR is a genuine anglegiven
• the chord and the third point lie on the given circleby Def.15
• the angle at the centre is twice the given angleby III.20

What it needs, and what needs it

Needs: III.20

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

Depth: 13 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 (×5)order
• the proof evaluates a different number of facts on different configurations (seen: [5, 6, 10]), so it is following more than one route through the diagramcase
• the 'collinear' fact (occurrence 2) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 1) is true in some configurations and false in otherscase

The proposition as code

@proposition(
    "III.34",
    CONSTRUCTION,
    sample=lambda rng: samples.points_round_a_circle(rng, 1) + samples.angle_config(rng),
)
def prop_III_34(o: Point, a: Point, p: Point, q: Point, r: Point) -> Out:
    """From the given circle, cut off a segment admitting the given angle."""
    hypothesis("the circle has positive radius", o != a)
    hypothesis("PQR is a genuine angle", not collinear(p, q, r), guard=True)
    around = circle(o, a, "the given circle")
    outline(p, q, r, close=False)

    # An angle at the circumference stands on twice its own arc, so the chord
    # cutting off the segment subtends twice the given angle at the centre.
    given = angle_at(p, q, r)
    b = posit(_turn(o, a, given.doubled()), "B")
    chord = line(a, b, "the chord cutting off the segment")
    third = posit(
        next(point for point in _round(o, a)
             if point not in (a, b) and not same_side(point, o, Line.through(a, b)))
        if not collinear(a, o, b) else _round(o, a)[0],
        "C",
    )
    outline(a, third, b, close=False)

    claim("the chord and the third point lie on the given circle", "Def.15",
          on_circle(b, around) and on_circle(third, around))
    # III.20 as encoded speaks of the segment where the angle at the centre is
    # twice the one at the circumference; on the other arc the doubled angle is
    # the reflex one, and the claim below allows for it.
    if not collinear(a, third, b) and angle_at(a, o, b) == angle_at(a, third, b).doubled():
        because(prop_III_20, o, a, third, b)

    claim("the angle at the centre is twice the given angle", "III.20",
          angle_at(a, o, b) == given.doubled()
          or angle_at(a, o, b) == STRAIGHT + STRAIGHT - given.doubled())
    return Out(chord=chord)