Book XII · Proposition 18

XII.18

Spheres are to one another in the triplicate ratio of their respective diameters.Heath, 1908

Every step, checked

• the two spheres are about one centre, and one is the greatergiven
• the lesser sphere has a positive radiusgiven
• the polyhedra inscribed in the two spheres are similar, so at every stage the enclosure holds the triplicate ratio of the diametersby XII.17
• and what is left over falls short of half itself at each stageby X.1
• therefore the spheres are to one another in the triplicate ratio of their diametersby XII.18

What it needs, and what needs it

Needs: X.1 XII.17

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

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

What it takes on trust

• a sphere is described, and XI Def. 14; no postulate describes a sphere (×2)solid

The proposition as code

@proposition("XII.18", THEOREM, sample=samples3.two_radii)
def prop_XII_18(o: Point3, a: Point3, b: Point3) -> Out:
    """Spheres are to one another in the triplicate ratio of their diameters."""
    hypothesis("the two spheres are about one centre, and one is the greater",
               sign(len2(o, a) - len2(o, b)) > 0)
    hypothesis("the lesser sphere has a positive radius", o != b)
    greater, lesser = length3(o, a), length3(o, b)
    sphere_through(o, a, "the greater sphere")
    sphere_through(o, b, "the lesser sphere")
    line3(o, a, "the radius of the greater")
    line3(o, b, "the radius of the lesser")

    because(prop_XII_17, o, a, b)

    for stage in GLOBE_STAGES:
        _drawn(polyhedron_in_sphere(o, greater, stage))

    ratio = greater / lesser
    found = squeeze(lambda stage: (sphere_bounds(o, greater, stage)
                                   / sphere_bounds(o, lesser, stage)),
                    ratio * ratio * ratio, GLOBE_STAGES)
    claim("the polyhedra inscribed in the two spheres are similar, so at every "
          "stage the enclosure holds the triplicate ratio of the diameters",
          "XII.17", found.held)
    claim("and what is left over falls short of half itself at each stage",
          "X.1", found.narrowing)
    claim("therefore the spheres are to one another in the triplicate ratio of "
          "their diameters", "XII.18", found.held and found.narrowing)
    return Out(enclosures=found.enclosures, ratio=ratio)