Book III · Proposition 5
If two circles cut one another, they will not have the same centre.Heath, 1908
Stated as a negative, and checked as one: two circles that cut cannot share a centre, because their radii would then have to be equal.
Needs: nothing earlier.
Rests on: Def.15
Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@proposition(
"III.5",
THEOREM,
sample=lambda rng: samples.points_round_a_circle(rng, 1) + (samples.nonzero(rng, 1, 3),),
note="Stated as a negative, and checked as one: two circles that cut cannot "
"share a centre, because their radii would then have to be equal.",
)
def prop_III_5(o: Point, a: Point, difference) -> Out:
"""A second circle on the same centre, of a different radius."""
hypothesis("the circle has positive radius", o != a)
hypothesis("the second radius differs from the first", sign(difference) != 0)
first = circle(o, a, "the first circle")
outer = posit(_along_from(o, a, length(o, a) + difference), "B")
second = circle(o, outer, "a second circle on the same centre")
# Cutting means sharing a point. Test that against the whole circumference,
# not against a convenient point or two: every point of either circle is
# checked against the other, and none of them lies on it.
claim("the two radii are unequal", "Def.15", not eq_len(o, a, o, outer))
claim("so no point of either circle lies on the other, and they never cut",
"Def.15",
not any(on_circle(point, second) for point in _round(o, a))
and not any(on_circle(point, first) for point in _round(o, outer)))
return Out()