Book XIII · Proposition 14

XIII.14

To construct an octahedron and comprehend it in a sphere, as in the preceding case; and to prove that the square on the diameter of the sphere is double of the square on the side of the octahedron.Heath, 1908

Every step, checked

• the sphere has a positive radiusgiven
• every vertex of the octahedron is on the sphereby XI.Def.14
• it is contained by eight equal and equilateral triangles, four edges meeting at each cornerby XI.Def.26
• and the square on the diameter of the sphere is double the square on the side of the octahedronby XIII.14

What it needs, and what needs it

Needs: XIII.13

Used by: XIII.15 XIII.18

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

Depth: 1 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.14", CONSTRUCTION, sample=samples3.sphere_about)
def prop_XIII_14(o: Point3, a: Point3) -> Out:
    """Construct an octahedron in a sphere, and prove the square on the diameter
    is double 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, _octahedron(), "an edge of the octahedron")

    because(prop_XIII_13, o, a)

    side2, across = _edge2(corners, edges), 4 * space_len2(o, a)
    claim("every vertex of the octahedron is on the sphere", "XI.Def.14",
          all(on_sphere(corner, globe) for corner in corners))
    claim("it is contained by eight equal and equilateral triangles, four edges "
          "meeting at each corner", "XI.Def.26",
          len(corners) == 6 and len(edges) == 12
          and _at_each_corner(corners, edges) == {4}
          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 double the square on "
          "the side of the octahedron", "XIII.14", across == 2 * side2)
    return Out(octahedron=corners, side2=side2, diameter2=across)