Book XIII · Proposition 17

XIII.17

To construct a dodecahedron and comprehend it in a sphere, like the aforesaid figures, and to prove that the side of the dodecahedron is the irrational straight line called apotome.Heath, 1908

Every step, checked

• the sphere has a positive radiusgiven
• the diameter of the sphere is rational, being the line every other is named againstgiven
• every vertex of the dodecahedron is on the sphereby XI.Def.14
• it is contained by twelve equal and equilateral pentagons, three edges meeting at each cornerby XI.Def.28
• and the side of the dodecahedron is the irrational straight line called apotomeby X.73
• its two terms are rational lines commensurable in square onlyby X.73

What it needs, and what needs it

Needs: X.73 XIII.16

Used by: XIII.18

Rests on: X.85-90, XI.Def.14, XI.Def.25, XI.Def.26, XI.Def.27, XI.Def.28

Depth: 4 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.17", CONSTRUCTION, sample=samples3.sphere_about)
def prop_XIII_17(o: Point3, a: Point3) -> Out:
    """Construct a dodecahedron in a sphere, and prove its side is the
    irrational straight line called apotome."""
    hypothesis("the sphere has a positive radius", o != a)
    hypothesis("the diameter of the sphere is rational, being the line every "
               "other is named against",
               is_rational_line(sqrt(4 * space_len2(o, a))))
    globe = sphere_through(o, a, "the given sphere")
    line3(o, a, "the radius")
    corners, edges = _figure(o, a, _dodecahedron(), "an edge of the dodecahedron")

    because(prop_XIII_16, o, a)

    side2, across = _edge2(corners, edges), 4 * space_len2(o, a)
    side = sqrt(side2 / across)
    named = classify(side)
    because(prop_X_73, named.terms[0], -named.terms[1])

    claim("every vertex of the dodecahedron is on the sphere", "XI.Def.14",
          all(on_sphere(corner, globe) for corner in corners))
    claim("it is contained by twelve equal and equilateral pentagons, three "
          "edges meeting at each corner", "XI.Def.28",
          len(corners) == 20 and len(edges) == 30
          and _at_each_corner(corners, edges) == {3}
          and all(space_len2(corners[i], corners[j]) == side2 for i, j in edges))
    claim("and the side of the dodecahedron is the irrational straight line "
          "called apotome", "X.73", named.family == "apotome")
    claim("its two terms are rational lines commensurable in square only",
          "X.73",
          len(named.terms) == 2
          and all(is_rational_in_square(term) for term in
                  (named.terms[0], -named.terms[1]))
          and not commensurable(named.terms[0], -named.terms[1]))
    return Out(dodecahedron=corners, side2=side2, side=side, name=named.name)