Book XII · Proposition 2

XII.2

Circles are to one another as the squares on the diameters.Heath, 1908

Every step, checked

• the four points are on one circle about the centregiven
• they are not all in one straight linegiven
• at every stage the figures inscribed in the two circles are similar, so the enclosure holds the ratio of the squares on the diametersby XII.1
• and what is left over falls short of half itself at each stage, so no other ratio can surviveby X.1
• therefore the circles are to one another as the squares on the diametersby XII.2

What it needs, and what needs it

Needs: X.1 XII.1

Used by: XII.11 XII.14

Rests on: VI.Def.1

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

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition("XII.2", THEOREM, sample=samples3.circle_in_space)
def prop_XII_2(o: Point3, a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Circles are to one another as the squares on their diameters."""
    hypothesis("the four points are on one circle about the centre",
               len2(o, a) == len2(o, b) == len2(o, c) == len2(o, d))
    hypothesis("they are not all in one straight line", not collinear3(a, b, c))
    because(prop_XII_1, o, a, b, c, d)

    normal = _axis_of((a, b, c))
    radius, ratio = length3(o, a), Fraction(5, 3)
    centre = posit3(Point3(o.x + 8, o.y, o.z), "P")
    for stage in STAGES:
        _ring(regular_polygon(o, radius, normal, stage))
        _ring(regular_polygon(centre, ratio * radius, normal, stage))

    squares = (4 * len2(o, a), 4 * ratio * ratio * len2(o, a))
    found = squeeze(
        lambda stage: (circle_bounds(o, radius, normal, stage)
                       / circle_bounds(centre, ratio * radius, normal, stage)),
        squares[0] / squares[1], STAGES)

    claim("at every stage the figures inscribed in the two circles are similar, "
          "so the enclosure holds the ratio of the squares on the diameters",
          "XII.1", found.held)
    claim("and what is left over falls short of half itself at each stage, so "
          "no other ratio can survive", "X.1", found.narrowing)
    claim("therefore the circles are to one another as the squares on the "
          "diameters", "XII.2", found.held and found.narrowing)
    return Out(enclosures=found.enclosures, squares=squares)