Book III · Proposition 8

III.8

If a point be taken outside a circle and from the point straight lines be drawn through to the circle, one of which is through the centre and the others are drawn at random, then, of the straight lines which fall on the concave circumference, that through the centre is greatest, while of the rest the nearer to that through the centre is always greater than the more remote, but, of the straight lines falling on the convex circumference, that between the point and the diameter is least, while of the rest the nearer to the least is always less than the more remote, and only two equal straight lines will fall on the circle from the point, one on each side of the least.Heath, 1908

The external twin of III.7. The same monotonicity, read from a point outside: distance grows steadily with the angle turned from the near end.

Every step, checked

• the circle has positive radiusgiven
• P lies outside the circlegiven
• of those falling on the concave circumference, that through the centre is greatestby I.20
• of those falling on the convex circumference, that between the point and the diameter is leastby I.20
• and of the rest, the nearer to the least is the lessby I.24
• only two equal lines fall from the point, one on each side of the leastby I.24

What it needs, and what needs it

Needs: I.20 I.24

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

Depth: 12 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 (×3)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×15)continuity

The proposition as code

@proposition(
    "III.8",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 1)
    + (1 + Fraction(rng.randint(2, 8), 4),),
    note="The external twin of III.7. The same monotonicity, read from a point "
    "outside: distance grows steadily with the angle turned from the near end.",
)
def prop_III_8(o: Point, a: Point, beyond) -> Out:
    """P is outside, on the diameter through A; A is the near end, D the far."""
    hypothesis("the circle has positive radius", o != a)
    hypothesis("P lies outside the circle", sign(beyond - 1) > 0)
    circle(o, a, "the given circle")
    far = posit(Point(o.x - (a.x - o.x), o.y - (a.y - o.y)), "D")
    p = posit(Point(o.x + beyond * (a.x - o.x), o.y + beyond * (a.y - o.y)), "P")
    line(p, far, "the line through the centre")

    reach = (a.x - o.x, a.y - o.y)
    turned = []
    for step in range(1, 5):
        half = Fraction(step, 4)
        cosine, sine = (1 - half * half) / (1 + half * half), 2 * half / (1 + half * half)
        turned.append(posit(
            Point(o.x + reach[0] * cosine - reach[1] * sine,
                  o.y + reach[0] * sine + reach[1] * cosine),
            f"P{step}",
        ))
    for point in turned:
        line(p, point)

    # Each line from P is the base of a triangle on a radius: I.20 bounds it,
    # and I.24 makes the wider angle at the centre give the longer base.
    for point in turned:
        because(prop_I_20, p, o, point)
    for nearer, further in zip(turned, turned[1:]):
        because(prop_I_24, o, p, further, o, p, nearer)

    claim("of those falling on the concave circumference, that through the centre "
          "is greatest", "I.20",
          all(sign(length(p, far) - length(p, point)) > 0 for point in turned + [a]))
    claim("of those falling on the convex circumference, that between the point and "
          "the diameter is least", "I.20",
          all(sign(length(p, point) - length(p, a)) > 0 for point in turned + [far]))
    claim("and of the rest, the nearer to the least is the less", "I.24",
          all(sign(length(p, turned[i + 1]) - length(p, turned[i])) > 0
              for i in range(len(turned) - 1)))
    mirrored = posit(_mirror_in(turned[0], o, a), "Q")
    line(p, mirrored)
    claim("only two equal lines fall from the point, one on each side of the least",
          "I.24",
          eq_len(p, turned[0], p, mirrored) and mirrored != turned[0])
    return Out(greatest=far, least=a)