Book XIII · Proposition 15

XIII.15

To construct a cube and comprehend it in a sphere, like the pyramid; and to prove that the square on the diameter of the sphere is triple of the square on the side of the cube.Heath, 1908

Every step, checked

• the sphere has a positive radiusgiven
• every vertex of the cube is on the sphereby XI.Def.14
• it is contained by six equal squares, three edges meeting at each cornerby XI.Def.25
• and the square on the diameter of the sphere is triple the square on the side of the cubeby XIII.15

What it needs, and what needs it

Needs: XIII.14

Used by: XIII.16 XIII.18

Rests on: XI.Def.14, XI.Def.25, XI.Def.26

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

What it takes on trust

• a sphere is described, and XI Def. 14; no postulate describes a spheresolid

The proposition as code

@proposition("XIII.15", CONSTRUCTION, sample=samples3.sphere_about)
def prop_XIII_15(o: Point3, a: Point3) -> Out:
    """Construct a cube in a sphere, and prove the square on the diameter is
    triple the square on the side."""
    hypothesis("the sphere has a positive radius", o != a)
    globe = sphere_through(o, a, "the given sphere")
    line3(o, a, "the radius")
    corners, edges = _figure(o, a, _cube(), "an edge of the cube")

    because(prop_XIII_14, o, a)

    side2, across = _edge2(corners, edges), 4 * space_len2(o, a)
    claim("every vertex of the cube is on the sphere", "XI.Def.14",
          all(on_sphere(corner, globe) for corner in corners))
    claim("it is contained by six equal squares, three edges meeting at each "
          "corner", "XI.Def.25",
          len(corners) == 8 and len(edges) == 12
          and _at_each_corner(corners, edges) == {3}
          and all(space_len2(corners[i], corners[j]) == side2 for i, j in edges))
    claim("and the square on the diameter of the sphere is triple the square on "
          "the side of the cube", "XIII.15", across == 3 * side2)
    return Out(cube=corners, side2=side2, diameter2=across)