Book XIII · Proposition 13

XIII.13

To construct a pyramid, to comprehend it in a given sphere, and to prove that the square on the diameter of the sphere is one and a half times the square on the side of the pyramid.Heath, 1908

Every step, checked

• the sphere has a positive radiusgiven
• every vertex of the pyramid is on the sphere, so it is comprehended in itby XI.Def.14
• it is contained by four equal and equilateral triangles, three edges meeting at each cornerby XI.Def.25
• and the square on the diameter of the sphere is one and a half times the square on the side of the pyramidby XIII.13

What it needs, and what needs it

Needs: nothing earlier.

Used by: XIII.14 XIII.18

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

Depth: 0 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.13", CONSTRUCTION, sample=samples3.sphere_about)
def prop_XIII_13(o: Point3, a: Point3) -> Out:
    """Construct a pyramid in a given sphere, and prove the square on the
    diameter is one and a half times 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, _tetrahedron(), "an edge of the pyramid")

    side2, across = _edge2(corners, edges), 4 * space_len2(o, a)
    claim("every vertex of the pyramid is on the sphere, so it is comprehended "
          "in it", "XI.Def.14", all(on_sphere(corner, globe) for corner in corners))
    claim("it is contained by four equal and equilateral triangles, three edges "
          "meeting at each corner", "XI.Def.25",
          len(corners) == 4 and len(edges) == 6
          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 one and a half times "
          "the square on the side of the pyramid", "XIII.13",
          2 * across == 3 * side2)
    return Out(pyramid=corners, side2=side2, diameter2=across)