Book III · Proposition 33

III.33

On a given straight line to describe a segment of a circle admitting an angle equal to a given rectilineal angle.Heath, 1908

Every step, checked

• A and B are distinctgiven
• PQR is a genuine anglegiven
• the given angle is neither zero nor straightgiven
• the circle described passes through both ends of ABby Def.15
• and the angle in the segment equals the given angleby III.21

What it needs, and what needs it

Needs: I.10 III.21

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

• 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 argument reads a 'same_side' fact off the figure (×8)order
• the proof evaluates a different number of facts on different configurations (seen: [11, 12]), 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 3) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 4) is true in some configurations and false in otherscase

The proposition as code

@proposition(
    "III.33",
    CONSTRUCTION,
    sample=lambda rng: samples.segment(rng) + samples.angle_config(rng),
)
def prop_III_33(a: Point, b: Point, p: Point, q: Point, r: Point) -> Out:
    """On AB, describe a segment admitting an angle equal to PQR."""
    hypothesis("A and B are distinct", a != b)
    hypothesis("PQR is a genuine angle", not collinear(p, q, r), guard=True)
    line(a, b, "the given line AB")
    outline(p, q, r, close=False)

    # An angle at the circumference is half the angle at the centre (III.20), so
    # the centre stands on the perpendicular bisector of AB where the half-chord
    # subtends the given angle: MA / MO is its tangent, and cos over sin gives
    # that exactly, without ever forming an angle in degrees.
    given = angle_at(p, q, r)
    hypothesis("the given angle is neither zero nor straight", not is_zero(given.sin))
    middle = posit(prop_I_10(a, b).midpoint, "M")
    across = _across(middle, a)
    centre = posit(
        Point(middle.x + (given.cos / given.sin) * across[0],
              middle.y + (given.cos / given.sin) * across[1]),
        "O",
    )
    described = circle(centre, a, "the segment described on AB")

    # The apex goes on the side the perpendicular points to, whichever side the
    # centre ended up on. For an acute angle the centre is on that side too and
    # the apex takes the greater arc; for an obtuse one the centre crosses over
    # and the apex takes the lesser, where the angle is the supplement of half
    # the angle at the centre -- which is the given angle again. A right angle
    # puts the centre on the chord and the two arcs agree.
    reaching = Line.through(middle, Point(middle.x + across[0], middle.y + across[1]))
    beyond = [
        point for point in meet(reaching, described)
        if sign((point.x - middle.x) * across[0]
                + (point.y - middle.y) * across[1]) > 0
    ]
    apex = posit(beyond[0], "C")
    outline(a, apex, b, close=False)

    alongside = [point for point in _round(centre, a)
                 if point not in (a, b, apex) and same_side(point, apex, Line.through(a, b))]
    if alongside:
        because(prop_III_21, centre, a, b, apex, alongside[0])

    claim("the circle described passes through both ends of AB", "Def.15",
          on_circle(a, described) and on_circle(b, described))
    claim("and the angle in the segment equals the given angle", "III.21",
          eq_angle(a, apex, b, p, q, r))
    return Out(circle=described, centre=centre, apex=apex)